theory String

imports List Main OrderedGroup

begin

typedef 'a string = "{x::'a list. True}"
apply auto
done

fun Occurs_CTl :: "'a => 'a list => nat" where
   "Occurs_CTl x [] = 0" |
   "Occurs_CTl x (xs # rest) = (Occurs_CTl x rest) + (if (xs = x) then 1 else 0)"


lemma JAC1:
"
(a # b) @ c = a # (b @ c)
"
apply auto
done

lemma JOCl1 :
"
Occurs_CTl x (y # z) = (Occurs_CTl x [y]) + (Occurs_CTl x z)
"

apply (induct z)
apply auto
done

lemma JOCl01:
"
Occurs_CTl x (y # z) = k ==> (Occurs_CTl x [y]) + (Occurs_CTl x z) = k
"
apply (insert JOCl1 [of x y z])
apply auto
done


lemma JOCl02:
"
(Occurs_CTl x [y]) + (Occurs_CTl x z) = k ==> Occurs_CTl x (y # z) = k 
"
apply (insert JOCl1 [of x y z])
apply auto
done

lemma JOCl2:
"
Occurs_CTl x (y @ z) = (Occurs_CTl x y) + (Occurs_CTl x z)
"
apply (induct y )
apply simp
apply (auto simp add: JAC1)
done

lemma JOCl3:
"
Occurs_CTl x [] = 0
"
apply auto
done

lemma JOC14 [dest, intro]:
"
ALL x. Occurs_CTl x Q = 0 ==> Q = []
"
apply (induct Q)
apply auto
apply (drule_tac x="a" in spec)
apply auto
done

lemma JOC15:
"
size a = listsum (map (% x. Occurs_CTl x [x]) a)
"
apply (induct a)
apply auto
done

fun remove :: "'a => 'a list => 'a list" where
  "remove x [] = []" |
  "remove x (y # ys) = (if y = x then (remove x ys) else y # (remove x ys))" 

lemma len1111 [simp]:
"
length (remove x xs) < Suc (length xs)
"
apply (induct xs)
apply auto
done

fun exSum :: "'a list => nat" where
 "exSum [] = 0" |
 "exSum (x # xs) =  (Occurs_CTl x (x # xs)) + (exSum (remove x xs))"

lemma JOC11115:
"
[|
a ~= b
|]
==> Occurs_CTl a (remove b c) = Occurs_CTl a c
"
apply (induct c)
apply auto
done

lemma JOC111115:
"
[|
b = a
|]
==> Occurs_CTl a (remove b c) = 0
"
apply (induct c)
apply auto
done


lemma JOC1115:
"
 exSum a2 = length a2
       ==> Occurs_CTl a1 a2 + exSum (remove a1 a2) = length a2
"
apply (induct a2)
apply auto
apply (simp add: JOC11115 JOC111115)
sorry

lemma JOC115:
"
length a = exSum a
"
apply (induct a)
apply auto
apply (simp add: JOC1115)
done

lemma JOCl5:
"
(ALL x. Occurs_CTl x P = Occurs_CTl x Q) --> size P = size Q
"
apply (simp add: JOC115)
apply (induct P)
apply clarsimp

apply (induct Q)
apply clarsimp
apply clarsimp
apply (drule_tac x="a" in spec)
apply clarsimp

apply (induct Q)
apply clarsimp
apply (rule_tac x="a" in exI)
apply clarsimp

apply clarsimp
sorry 
(*
apply (auto simp add: JOC15)
apply (rule classical)
apply auto


apply (induct P)
apply clarsimp
apply (simp add: JOC14)
apply (rule allI)
apply (simp add: JOCl1)
apply auto
apply (drule_tac x="Q" in spec)
apply clarsimp
*)

lemma Abs_string_inverse [simp]:
"
Rep_string (Abs_string y) = y
"
apply (insert string_def)
apply (rule Abs_string_inverse)
apply auto 
done

constdefs length :: "'a string => nat"
          "length a == size (Rep_string a)"
          is_empty_string :: "'a string => bool"
          "is_empty_string a == size (Rep_string a) = 0"
          empty_string :: "'a string"
          "empty_string == Abs_string []"
          ext :: "'a => 'a string => 'a string"
          "ext x a == Abs_string (x # (Rep_string a))"
          cat :: "'a string => 'a string => 'a string" (infix "concate" 66)
          "a concate x == Abs_string ( (Rep_string a) @ (Rep_string x))"
          Occurs_Ct :: "'a => 'a string => nat"
          "Occurs_Ct x a == Occurs_CTl x (Rep_string a)"
          IsPermutation :: "'a string => 'a string => bool"
          "IsPermutation a b == (ALL x. (Occurs_Ct x a) = (Occurs_Ct x b))"
          PartBtwn :: "nat => nat => 'a string => 'a string"
          "PartBtwn m n a == Abs_string (sublist (Rep_string a) {x. x >= m & x < n}) " 
          DeString :: "'a string => 'a"
          "DeString a == last (Rep_string a)"
          Stringleton :: "'a => 'a string" ("<_>")
          "Stringleton x == Abs_string ([x])"
          reverse ::"'a string => 'a string"
          "reverse a == Abs_string (rev (Rep_string a))"
          elementof :: "'a => 'a string => bool"
          "elementof x a == x : (set (Rep_string a))"
          Is_SubString :: "'a string => 'a string => bool"
          "Is_SubString a b == (EX x y. (x concate a) concate y = b)"  

translations
 "a o b" == "a concate b"

lemma Rep_Cat1 [simp]:
"
Rep_string (x o y) = (Rep_string x) @ (Rep_string y)
"
apply (simp add: cat_def Rep_string_inverse Abs_string_inverse)
done

lemma Rep_Cat2 [simp]:
"
Rep_string ((Abs_string x) o y) = x @ (Rep_string y)
"
apply (simp add: Rep_Cat1)
done

lemma Rep_Cat3 [simp]:
"
Rep_string ( x o (Abs_string y)) = (Rep_string x) @  y
"
apply (simp add: Rep_Cat1)
done

lemma Rep_String1 [simp]:
"
Rep_string <y> = [y]
"
apply (simp add: Stringleton_def)
done

lemma Rep_Ext1 [simp]:
"
Rep_string (ext x a) = x # (Rep_string a)
"
apply (induct a)
apply (simp add: ext_def Abs_string_inverse)
done

lemma Abs_Ext1:
"
Abs_string (x # a) = ext x (Abs_string a)
"
apply (induct a)
apply (simp add: ext_def Abs_string_inverse Rep_String1)+
done


lemma Abs_string_inverse_inject [simp]:
"
Rep_string (Abs_string x) =  Rep_string (Abs_string y) ==> x = y
"
apply (simp add: Abs_string_inverse)
done

lemma Abs_string_inject1 [dest!]:
"
Abs_string x = Abs_string y ==> x = y
"
apply (subgoal_tac "Rep_string (Abs_string x) = Rep_string (Abs_string y)")

apply simp+
done

lemma Abs_string_inject2 [intro]:
"
x = y ==> Abs_string x = Abs_string y 
"
apply auto
done

lemma ExtProp1 [simp]:
"
ext x a ~= empty_string
"
apply (auto simp add: ext_def empty_string_def Rep_Ext1)
done

lemma ExtProp2 [dest]:
"
[|
 ext x a = ext y b
|]
==> x = y & a = b
"
apply auto
apply (auto simp add: ext_def)
apply (insert Abs_string_inject1 [of " x # (Rep_string a)" " y # (Rep_string b)"])
apply auto
apply (simp add: Rep_string_inject)
done

lemma Stringleton1 [simp]:
"
<x> ~= empty_string
"
apply (auto simp add: Stringleton_def empty_string_def Rep_string_inverse Abs_string_inverse Abs_string_inject1)
done


lemma CatProp1 [simp]:
"
(a::'a string) o empty_string = a
"
apply (auto simp add: cat_def empty_string_def Abs_string_inverse Rep_string_inverse)
done

lemma CatProp11 [simp]:
"
empty_string o (a::'a string) = a
"
apply (auto simp add: cat_def empty_string_def Abs_string_inverse Rep_string_inverse)
done

lemma CatProp3 [iff]:
"
((a::'a string) o (b o c)) = ((a o b) o c)
"
apply (auto simp add: cat_def Abs_string_inverse Rep_string_inverse)
done


lemma test1:
"
((a o b) o c) = ((a::'a string) o (b o c))
"
apply auto
done

lemma CatProp31:
"
(((a::'a string) o b) o c) = (a o (b o c))
"
apply (auto simp add: cat_def Abs_string_inverse Rep_string_inverse)
done

lemma CatProp4 [dest]:
"
((a::'a string) o b = c o b) ==> a = c
"
apply (auto simp add: cat_def)
apply (auto simp add:  Rep_string_inject)
done

lemma CatProp41 [dest]:
"
(b o (a::'a string) = b o c) ==> a = c
"
apply (auto simp add: cat_def)
apply (auto simp add:  Rep_string_inject)
done

lemma LengthProp3 [dest]:
"
[|
 (a::'a string) o b = g o d;
 length b = length d
|]
==>
 b = d & a = g
"
apply (simp add: cat_def length_def)
apply (drule Abs_string_inject1)
apply (simp add: Rep_string_inject)
done

lemma JLengthEmpty1:
"
(q = empty_string ) ==> (length q = 0)
"
apply (auto simp add: empty_string_def length_def)
done

lemma JLengthEmpty2:
"
(length q = 0) ==> (q = empty_string )
"
apply (auto simp add: empty_string_def length_def)
apply (subgoal_tac "Abs_string (Rep_string q) = Abs_string []")
apply (insert Rep_string_inverse [of q])
apply simp
apply auto
done

lemma JLengthEmpty21 [iff]:
"
(length q = 0) = (q = empty_string )
"
apply (auto simp add: JLengthEmpty2 JLengthEmpty1)
done


lemma JLengthEmpty3:
"
(q ~= empty_string ) ==> (length q > 0)
"
apply (erule contrapos_np)
apply (auto simp add: JLengthEmpty2);
done



lemma JLengthEmpty4:
"
(length q > 0) ==> (q ~= empty_string )
"
apply (erule contrapos_pn)
apply (auto simp add: JLengthEmpty1)
done

lemma JLengthEmpty [iff]:
"
(length q > 0) = (q ~= empty_string )
"
apply auto
apply (simp add: length_def empty_string_def Abs_string_inverse JLengthEmpty3)
apply (drule JLengthEmpty3)
apply auto
done

lemma JLength1 [iff]:
"
(length q ~= 0) = (length q > 0)
"
apply auto
done

lemma JLength [iff]:
"
length (x o y) = (length x) + (length y)
"
apply (simp add: cat_def length_def)
done

lemma JLengthSingleton [simp]:
"
length <x> = 1
"
apply (simp add: Stringleton_def length_def)
done

lemma JCat1:
"
empty_string o x = x
"
apply (auto simp add: empty_string_def cat_def Abs_string_inverse Rep_string_inverse)
done

lemma JCat2:
"
x o empty_string = x
"
apply (auto simp add: empty_string_def cat_def Abs_string_inverse Rep_string_inverse)
done

lemma JOC1 [iff]:
"
Occurs_Ct x ((y::'a string) o z) = (Occurs_Ct x z) +  (Occurs_Ct x y)
"
apply (simp add: Occurs_Ct_def Rep_Cat1)
apply (simp add: JOCl2)
done

lemma JRev [simp]:
"
reverse (reverse a) = a
"

apply (simp add: reverse_def Abs_string_inverse Rep_string_inverse)
done

lemma JRevCat:
"
(reverse p) o <x> = reverse (<x> o p)
"
apply (simp add: reverse_def cat_def Stringleton_def Abs_string_inverse Rep_string_inverse)
done

lemma JRevCat1 [iff]:
"
reverse (q o p) = (reverse p) o (reverse q)
"
apply (simp add: reverse_def cat_def Stringleton_def Abs_string_inverse Rep_string_inverse)
done

lemma JRevEmpty [simp]:
"
reverse empty_string = empty_string
"
apply (simp add: reverse_def empty_string_def  Abs_string_inverse Rep_string_inverse)
done

lemma JRevStringleton [simp]:
"
reverse <x> = <x>
"
apply (simp add: reverse_def empty_string_def  Abs_string_inverse Rep_string_inverse Stringleton_def)
done


lemma JRevNE [iff]:
"
reverse (ext x a) = (reverse a) o <x>
"
apply (auto simp add: reverse_def ext_def cat_def Stringleton_def Abs_string_inverse Rep_string_inverse)
done

lemma JRevDef:
"
reverse empty_string = empty_string &
reverse (ext x a) = (reverse a) o <x>
"
apply auto
done

interpretation semigroup_cat: semigroup_add ["cat"]
apply unfold_locales 
apply (auto)
done 

interpretation monoid_cat: monoid_add ["empty_string" "cat"]
apply unfold_locales 
apply auto
done 

interpretation cancel_semigroup_cat: cancel_semigroup_add ["cat"]
apply unfold_locales 
apply (erule  CatProp41)
apply (erule CatProp4)
done

lemma ACLeft [iff]:
"
(x::'a string) o (y o z) = (x o y) o z
"
apply (insert semigroup_cat.add_assoc[of x y z] )
apply auto
done

lemma JSubstringProp2R [simp]:
"
(Is_SubString a a)
"
apply (auto simp add: Is_SubString_def)
apply (rule_tac x="empty_string" in exI)+
apply (auto simp add: JCat1 JCat2)
done

lemma JSubstringProp2T [dest]:
"
[|
(Is_SubString a b);
(Is_SubString b c)
|]
==> (Is_SubString a c)
"
apply (auto simp add: Is_SubString_def)
apply (rule_tac x="xa o x" in exI)
apply (rule_tac x="y o ya" in exI)
apply auto
done

lemma JSubstringProp2AS [dest, intro]:
"
[|
(Is_SubString a b);
(Is_SubString b a)
|]
==> a = b
"
apply (simp add: Is_SubString_def)
apply auto
apply (auto simp add: cat_def)

sorry

lemma JSubstringProp3:
"
(Is_SubString a b) ==> Occurs_Ct y a <= Occurs_Ct y b
"
apply (auto simp add: Is_SubString_def)
done


lemma JSubstringProp4:
"
(Is_SubString a b) ==> length a <= length b
"
apply (auto simp add: Is_SubString_def length_def)
done

consts
    IsNondecreasing :: "'a string => bool"
    IsASmallest :: "'a string => 'a => bool"

context linorder
begin

fun IsNondecreasing :: "'a string \<Rightarrow> bool" where
  "IsNondecreasing x = sorted (Rep_string x)"

lemma ND1 [simp]:
"
IsNondecreasing empty_string
"
apply (auto simp add: empty_string_def)
done

lemma ND2 [simp]:
"
IsNondecreasing <y>
"
apply (auto simp add: Stringleton_def)
done

fun IsASmallestl::"'a list => 'a => bool" where
   "IsASmallestl [] m = True" |
   "IsASmallestl [x] m = (m <= x)" |
   "IsASmallestl (x # y) m = ((m <= x) & (IsASmallestl y m))"

lemma JList1:
"
IsASmallestl q m ==> ALL x. (EX y z. q = (y @ [x] @ z) --> m <= x)
"
apply auto
done

lemma JList2:
"
IsASmallestl (p # q) m == (IsASmallestl [p]  m) & (IsASmallestl q m)
"
apply auto
apply (induct q)
apply simp
apply simp
done

lemma JList21:
"
 IsASmallestl (p # q) m
==> (IsASmallestl [p]  m) & (IsASmallestl q m)
"
apply auto
apply (induct q)
apply simp
apply simp

apply (induct q)
apply simp 
apply simp 
done

lemma JList3:
"
IsASmallestl (p @ q) m == (IsASmallestl p  m) & (IsASmallestl q m)
"
apply (induct p)
apply simp
apply simp
apply (insert JList2)
apply simp
done

lemma JList4:
"
IsASmallestl (p @ q) m = IsASmallestl (q @ p) m
"
apply (auto simp add: JList3)
done

lemma JList5:
"
[|
 IsASmallestl q min1;
 x <= min1
|]
==>
 IsASmallestl (q @ [x]) x
"
apply (auto simp add: JList3)
apply (induct q)
apply auto
apply (insert JList2)
(*sledgehammer *)
apply (metis IsASmallestl.simps(2) JList2 leD less_le_trans not_le)
done

lemma JList6:
"
[|
 IsASmallestl q min1;
 ~ (x <= min1)
|]
==>
 IsASmallestl (q @ [x]) min1
"
apply (auto simp add: JList3)
done

fun IsASmallest::"'a string => 'a => bool" where
  "IsASmallest a m = IsASmallestl (Rep_string a) m"

lemma IsASmallestProp0:
"
IsASmallest (x o y) a == (IsASmallest x a) & IsASmallest y a
"
apply (auto simp add: JList3)
done

lemma IsASmallestProp01 [intro]:
"
(IsASmallest x a) & IsASmallest y a ==> IsASmallest (x o y) a
"
apply (auto simp only: IsASmallestProp0)
done

lemma IsASmallestProp1:
"
IsASmallest (x o y) a == IsASmallest (y o x) a
"
apply (insert JList4 [of "Rep_string x" "Rep_string y" a])
apply auto
done

lemma IsASmallestProp2 [elim!]:
"
[|
 IsASmallest q min1;
 x <= min1
|]
==>
 IsASmallest (q o <x>) x
"
apply (auto simp add: JList5)
done

lemma IsASmallestProp3 [elim!]:
"
[|
 IsASmallest q min1;
 ~ (x <= min1)
|]
==>
 IsASmallest (q o <x>) min1
"
apply (auto simp add: JList6)
done

lemma IsASmallestProp31 [elim!]:
"
[|
 IsASmallest (q o <min1>) min1;
 ~ (x <= min1)
|]
==>
 IsASmallest (q o <x>) min1
"
apply (rule IsASmallestProp3)
defer
apply clarsimp
apply (simp only: IsASmallestProp0)
done

lemma JSmallStringleton [simp]:
"
IsASmallest <m> m 
"
apply auto
done

lemma JStringND:
"
 IsNondecreasing (a::'a string) ==> (ALL (b::'a string) (c::'a string) (x::'a) (y::'a). a = b o ((<x>) o ((<y>) o c)) --> x <= y)
"
apply (auto simp add: IsNondecreasing.simps)
apply (simp add: sorted_append sorted_Cons)
done

lemma ND3 [intro] :
"
[|
 IsNondecreasing (a);
 IsASmallest a y
|]
  ==> IsNondecreasing (<y> o a)
"
apply (auto simp add: elementof_def Stringleton_def)
sorry

lemma ND4 [intro!]:
"
[|
 IsNondecreasing (a o <y>);
 y <= b
|]
  ==> IsNondecreasing ((a o <y>) o <b>)
"
apply auto
sorry

lemma ND5 [intro]:
"
[|
 Is_SubString <x> Q;
 IsASmallest Q min1
|]
  ==> min1 <= x
"
apply auto
sorry


lemma JStringSmall:
"
IsASmallest q m ==> ALL x. (EX y z. q = y o (<x> o z) --> m <= x)
"
apply auto
apply (insert JList1 [of "Rep_string q" m])
apply auto
apply (drule_tac x=x in spec)
apply (auto )
apply (drule_tac x="Abs_string y" in spec)
apply (drule_tac x="Abs_string z" in spec)
apply auto
done

lemma JSublist1:
"
Q = sublist Q {j. j < size Q}
"
apply (induct Q)
apply (auto simp add: sublist_Cons)
done

lemma JSublist2:
"
Q = (sublist Q {0} ) @ (sublist Q  {x. x >= 1 & x < (size Q)})
"
apply (induct Q)
apply simp
apply (auto simp add: sublist_Cons JSublist1)
done


lemma JSublist3:
"
(sublist Q {0} ) @ (sublist Q  {x. x >= 1 & x < (size Q)}) = Q
"
apply (insert JSublist2 [of Q])
apply auto
done


lemma JPBTW1 [iff]:
"
Q = (PartBtwn 0 1 Q) o (PartBtwn 1 (length Q) Q)
"
apply (auto simp add: PartBtwn_def length_def Rep_Cat1) 
apply (auto simp add: cat_def Abs_string_inverse)
apply (insert JSublist3 [of "Rep_string Q"])
apply (auto simp add: Rep_string_inverse)
done

lemma JPBTW2:
"
(PartBtwn 0 1 Q) o (PartBtwn 1 (length Q) Q) = Q
"
apply (insert JPBTW1 [of Q])
apply auto
done

lemma OccursCtProp1:
"
(y = x --> Occurs_Ct y <x> = 1 ) & (y ~= x --> Occurs_Ct y <x> = 0)
"
apply (auto simp add: Occurs_Ct_def Stringleton_def Abs_string_inverse)
done

lemma OccursCtProp1 [iff]:
"
Occurs_Ct y ((a::'a string) o b) = Occurs_Ct y (a::'a string) + Occurs_Ct y b
"
apply (auto simp add: Occurs_Ct_def)
apply (auto simp add: JOCl2)
done

lemma OccursCtProp03:
"
Occurs_CTl y (rev x) = Occurs_CTl y x
"
apply (induct x)
apply simp
apply simp
apply (subst JOCl2)
apply (subst JOCl2)
apply auto
done

lemma OccursCtProp3 [simp]:
"
Occurs_Ct y (reverse (a::'a string) ) = Occurs_Ct y a 
"
apply (auto simp add: Occurs_Ct_def reverse_def OccursCtProp03)

done


lemma OccursCtProp04:
"
size a = listsum (map (% x. Occurs_CTl x a) a)
"
apply (induct a)
apply simp
apply auto
sorry

lemma OccursCtProp4:
"
length a = listsum (map (% x. Occurs_Ct x a) (Rep_string a))

"
apply (auto simp add: Occurs_Ct_def length_def OccursCtProp04)
done


lemma JPER2 [simp]:
"
IsPermutation (x o y) (y o x)
"
apply (auto simp add: IsPermutation_def )
(* apply (auto simp add: JOC1)*)
done

(*
lemma BPer3A:
"
IsPermuation b c = IsPermutation (a o b o d) (a o c o d)
"

lemma BPer3B:
"
IsPermuation b c = IsPermutation (a o b) (a o c)
"

lemma BPer3C:
"
IsPermuation b c = IsPermutation (b o d) (c o d)
"
*)

lemma JPER5 [simp]:
"
IsPermutation Q Q
"
apply (auto simp add: IsPermutation_def Occurs_Ct_def)
done

lemma JPER21 [intro]:
"
IsPermutation (x o y) Q ==> IsPermutation (y o x) Q
"
apply (auto simp add: IsPermutation_def )
(*apply (auto simp add: JOC1)*)
apply (drule_tac x="xa" in spec)
apply auto
done

lemma JPER2101 [dest]:
"
[|
IsPermutation P Q;
IsPermutation Q R
|]
==>
IsPermutation P R
"
apply (auto simp add: IsPermutation_def Occurs_Ct_def)
done

lemma JPER211 [dest]:
"
IsPermutation (x o y) Q ==>  Is_SubString x Q & Is_SubString y Q
"
sorry


lemma JPER22:
"
IsPermutation (x o (y o z)) Q = IsPermutation (x o (z o y)) Q
"
apply (auto simp add: JPER2)
apply (auto simp add: IsPermutation_def )
(*apply (auto simp add: JOC1)*)
apply (drule_tac x="xa" in spec)
apply auto
apply (drule_tac x="xa" in spec)
apply auto
done

lemma JPER221 [intro, dest]:
"
IsPermutation (x o (y o z)) Q ==> IsPermutation (x o (z o y)) Q
"
apply (subst JPER22)
apply clarify
done

lemma JPER003 [dest]:
"
ALL x. Occurs_CTl x Q = 0 ==> Q = []
"
apply (induct Q)
apply auto
apply (drule_tac x="a" in spec)
apply auto
done

lemma JPER0003 [intro]:
"
 Q = [] ==> (ALL x. Occurs_CTl x Q = 0)
"
apply (induct Q)
apply auto
done

lemma JPER013:
"
Occurs_CTl x P > 0 --> x : set P
"

apply (induct P)
apply simp
apply (simp add: JOCl1)
done

lemma JPER023:
"
Occurs_CTl x P > 0 --> x : set P
"
apply (induct P)
apply (auto simp add: JOCl1)
done

lemma JPER03:
"
(ALL x. Occurs_CTl x P = Occurs_CTl x Q) =  (size P = size Q)
"
sorry
(*
apply (induct Q)
apply (simp add: JOCl3)
defer
apply (induct P)
defer
defer
apply safe
apply (simp add: JPER003)
apply clarsimp
apply (drule_tac x="a" in spec)+
apply (clarsimp)+

apply (drule_tac x="aa" in spec)+
apply clarsimp

apply clarsimp

apply clarsimp
apply (subst JOCl1)



apply auto



apply (rule impI)
apply (simp del: Occurs_CTl.simps)
apply (rule classical)
apply (simp del: Occurs_CTl.simps)
apply auto
defer
apply (drule_tac x="a" in spec)
apply auto

sorry
*)
lemma JPER13 [elim]:
"
IsPermutation P Q ==> length P = length Q
"
apply ( simp add: IsPermutation_def)
apply (auto simp add: length_def)
apply (auto simp add: Occurs_Ct_def)

apply (auto simp add: JPER03)
done

lemma JPER3 [intro]:
"
IsPermutation (x o y) Q ==> (length x) + (length y) = (length Q)
"
apply (auto simp add: IsPermutation_def)
(*apply (simp add: JOC1)*)
apply (auto simp add: length_def)
apply (auto simp add: Occurs_Ct_def)
sorry


lemma JPER4 [intro]:
"
IsPermutation (x o y) Q ==> (length x) <= (length Q)
"
apply (auto dest: JPER3)
done

lemma JPER40 [intro]:
"
IsPermutation (x o y) Q ==> (length y) <= (length Q)
"
apply (auto dest: JPER3)
done


lemma JPER41:
"
[|
IsPermutation (x o y) Q;
y = z o <m>
|]
 ==> (length x) < (length Q)
"
apply (insert JPER3 [of x y Q])
apply (auto del: JPER3)
done

lemma JPER410:
"
[|
IsPermutation (x o y) Q;
x = z o <m>
|]
 ==> (length y) < (length Q)
"
apply (insert JPER3 [of x y Q])
apply (auto del: JPER3)
done

lemma JPER411 [dest, elim]:
"
[|
IsPermutation (x o y) Q;
length y > 0
|]
 ==> (length x) < (length Q)
"
apply (drule JPER3)
apply arith
done

lemma JPER412 [dest, elim]:
"
[|
IsPermutation (x o y) Q;
length x > 0
|]
 ==> (length y) < (length Q)
"
apply (drule JPER3)
apply arith
done

lemma JPER42 [intro]:
"
[|
IsPermutation (x o <y>) Q
|]
 ==> (length x) < (length Q)
"
apply auto
done

lemma JPER43 [intro]:
"
[|
IsPermutation (<x> o y) Q
|]
 ==> (length y) < (length Q)
"
apply auto
done


lemma JPER6 [dest]:
"
[|
 IsPermutation P Q;
 IsPermutation Q R
|]
==>
 IsPermutation P R
"
apply (auto simp add: IsPermutation_def Occurs_Ct_def)
done

lemma JPER7 [intro]:
"
IsPermutation P Q ==> IsPermutation Q P
"
apply (auto simp add: IsPermutation_def Occurs_Ct_def)
done

lemma JPER8 [intro]:
"
[|
IsPermutation P Q;
IsASmallest P x
|]
==> IsASmallest Q x
"
sorry

(*
apply (insert JPER13[ of P Q])
apply clarify
apply (simp only: IsPermutation_def IsASmallest.simps length_def Occurs_Ct_def)


apply (induct "Rep_string Q")

apply clarsimp

apply (subst JList2)

apply simp

apply auto

apply (rule classical)
apply auto
apply (drule_tac x=x in spec)
apply auto


apply (rule allI)
apply (rule impI)
apply (drule_tac x="ext a P" in spec)


apply (induct "Rep_string P")
apply clarsimp


apply clarsimp

apply (simp only: JList21)
apply (drule JList21)
apply auto



apply (drule JList21)+


done
*)


end

declare IsASmallest.simps[ simp del]
declare IsNondecreasing.simps[ simp del]

end