theory String

imports List Main OrderedGroup

begin

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

lemma Abs_string_inverse [simp]:
"
Rep_string (Abs_string y) = y
"
apply (insert string_def)
apply (rule Abs_string_inverse)
apply auto 
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

constdefs empty_string :: "'a string"
          "empty_string == Abs_string []"
          ext :: "'a string => 'a => 'a string"
          "ext a x == Abs_string (x # (Rep_string a))"

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

lemma CAxiom1 [simp]:
"
empty_string ~= ext a x
"
apply (insert Axiom1 [of a x])
apply (erule contrapos_nn)
apply auto
done

lemma Axiom2 [dest]:
"
ext s1 x1 = ext s2 x2 ==> x1 = x2 & s1 = s2
"
apply (simp add: ext_def)
apply auto
apply (simp add: Rep_string_inject)
done

lemma LAxiom3 [intro]:
"
[|
 P [];
 ALL x a. P a --> P (x # a)
|]
==>
 P x
"
apply (induct x)
apply auto
done


lemma LAxiom31:
"
P (Abs_string x) ==> EX K. K x = P (Abs_string x)
"
apply auto
done

lemma LAxiom32:
"
EX K. (ALL x. P (Abs_string x) =  K x )
"
apply auto
done

lemma Axiom3:
"
[|
 P empty_string;
 ALL a x. P a --> P (ext a x)
|]
==> P x
"
apply (unfold empty_string_def ext_def)
(* A little more work *)
apply auto
apply (induct x)

apply (insert LAxiom32 [of P])
apply auto
apply (frule_tac x="y" in spec)
apply simp
apply (rule LAxiom3)
apply auto
done

(*function length :: "'a string => nat"
 where
   "length empty_string = 0" 
   | "length (ext x a) = 1 + length a"
apply elim_to_cases
apply auto
done
termination 
apply (relation "measure (%(x,a). )"
sorry
*)

(* This axiom ensures that the termination proofs go through *)
constdefs
  len :: "'a string => nat"
  "len a == (size (Rep_string a))"
  length :: "'a string => int" ("|_|" 55)
  "length a == of_nat (len a)"


lemma Axiom4 [iff]:
"
len empty_string = 0 & len (ext a x) = 1 + len a
"
apply (rule Axiom3)
apply (auto simp add: empty_string_def ext_def len_def)
done

lemma LengthDef [iff]:
"
length empty_string = 0 & length (ext a x) = 1 + length a
"
apply (rule Axiom3)
apply (auto simp add:  length_def)
done
(* Past this point, the string definition is never expanded *)

lemma LengthGZ [simp]:
"
length a >= 0
"
apply (rule Axiom3)
apply (auto)
done


lemma LengthGZ1 :
"
length a < 0 --> False
"
apply (rule Axiom3)
apply auto
done

lemma LengthGZ1 [dest]:
"
length a < 0 ==> False
"
apply (insert LengthGZ1[of a])
apply auto
done


(* Added ot Original Theory*)

lemma LengthGZ01 [intro]:
"
x <= 0 ==> x <= length a
"
apply (rule classical)
apply auto
apply (rule_tac a=a in LengthGZ1)

apply auto
done

(* Added ot Original Theory end*)

lemma Length1[dest]:
"
length x > 0 ==> x ~= empty_string
"
apply auto
done

lemma Length2:
"
 x ~= empty_string --> length x > 0 
"
apply (rule Axiom3)
apply auto
done

lemma Length2 [dest]:
"
 x ~= empty_string ==> length x > 0 
"
apply (insert Length2 [of x])
apply auto
done

lemma Length3 [dest]:
"
length x = 0 ==> x = empty_string
"

apply (erule contrapos_pp)
apply auto
done

lemma ExEq [intro]:
"
[|
 a = b;
 x = y
|]
==>
ext a x = ext b y
"
apply auto
done

lemma ExNES:
"
y ~= empty_string --> (EX x a. y = ext a x)
"
apply (rule Axiom3)
apply simp
apply (rule allI, rule allI, rule impI)
apply auto
done

lemma ExNES:
"
y ~= empty_string ==> (EX x a. y = ext a x)
"
apply (insert ExNES[of y])
apply auto
done


lemma ALLNotExEmpty [dest]:
"
(ALL x a. y ~= ext a x) ==> y = empty_string
"
apply (cases "y = empty_string")
apply auto
apply (drule ExNES)
apply auto
done

constdefs Stringleton :: "'a => 'a string" ("<_>")
          "Stringleton x == ext empty_string x" 

function cat :: "'a string => 'a string => 'a string" (infix "concate" 55)
 where
    "cat a empty_string  = a"
  | "cat a (ext b x ) = ext (cat a b) x"
apply elim_to_cases
apply (auto dest: Axiom2)
apply (rule ALLNotExEmpty)
apply auto
done

termination
apply (relation "measure (%(x,a). (len(a)))") 
apply auto
done

function reverse :: "'a string => 'a string"
where
  "reverse empty_string = empty_string"
 |"reverse (ext a x) =  cat <x>  (reverse a)"
apply elim_to_cases
apply (auto dest: Axiom2)
apply (intro ALLNotExEmpty)
apply auto
done

termination
apply (relation "measure (%(x). len(x))") 
apply auto
done

translations
 "a * b" == "(a concate b)"
 "a o b" == "a concate b"

lemma CatExt [intro]:
"
ext a x = cat a <x>
"
apply (simp add: Stringleton_def)
done

lemma Stringleton1 [simp]:
"
<x> ~= empty_string
"
apply (simp add: Stringleton_def Axiom1)
done

lemma CatProp1 [simp]:
"
(a::'a string) * empty_string = a
"
apply (rule Axiom3)
apply auto
done

lemma CatProp11 [simp]:
"
empty_string * (a::'a string) = a
"
apply (rule Axiom3)
apply auto
done

(* Added to Original Theory *)
lemma CatProp12 [dest]:
"
a * b = empty_string ==> a = empty_string & b = empty_string
"
apply (induct a b rule: cat.induct)
apply auto
done
(* Added to Original Theory End*)


lemma CatProp3 [iff]:
"
((a::'a string) * (b * c)) = ((a * b) * c)
"
apply (induct b c rule: cat.induct)
apply auto
done

lemma CatProp31:
"
(((a::'a string) * b) * c) = (a * (b * c))
"
apply (induct b c rule: cat.induct)
apply auto
done

lemma ExtSuc [simp]:
"
ext b x ~= b
"
apply (rule Axiom3)
apply auto
done

lemma ExtSuc1 [simp]:
"
 b ~= ext b x
"
apply (rule Axiom3 [of "%y. y ~= ext y x"])
apply auto
done

lemma CatNonEmpty:
"
a * b ~= b ==> a ~= empty_string
"
apply auto
done

lemma ExtCatEq:
"
ext (a * b) x  = a * (ext b x) 
"
apply auto
done

lemma CatEmpty1:
"
b = a * b --> a = empty_string
"
apply (rule Axiom3 [of "%x.  x = a * x --> a = empty_string"])

apply auto
done

lemma CatEmpty1 [dest]:
"
b = a * b ==> a = empty_string
"
apply (insert CatEmpty1[of b a])
apply auto
done


lemma LengthCat [iff]:
"
length (a * b) = length a + length b
"
apply (rule Axiom3 [of "%x. length (a * x) = length a + length x"])
apply auto
done

(* Added to Original Theory *)

lemma LengthCat1 :
"
length (a * b) =  c ==> length a + length b = c
"
apply auto
done

lemma LengthCat2 :
"
c = length (a * b)  ==> c = length a + length b 
"
apply auto
done

lemma CatLength:
"
q = a * b ==> length q = length a + length b
"
apply auto
done
(* Added to Original Theory end*)

lemma LengthExt [iff]:
"
length (ext a x) = length a + 1
"
apply (rule Axiom3 )
apply auto
done


lemma CatEmpty [dest]:
"
b * a = b ==> a = empty_string
"
apply (induct b a rule: cat.induct)
apply clarsimp

apply (rule classical)
apply simp

apply (subgoal_tac "length (ext (a * b) x) = length a")
defer
apply clarsimp


apply (erule contrapos_pp)
apply (simp only: LengthExt)
apply auto

apply (subgoal_tac "length b < 0")
apply (drule LengthGZ1)
apply auto

(* foo *)
done


lemma ExtCancel1[intro]:
"
x = y & a = b ==> ext a x = ext b y 
"
apply auto
done


lemma CatEmpty2 [dest]:
"
 a * b = b ==> a = empty_string
"
apply (insert CatEmpty1 [of b a])
apply auto
done

lemma CatProp4:
"
((a::'a string) * b = c * b) --> a = c
"
apply (rule Axiom3 [of "%x. a * x = c * x --> a = c"])
apply auto
done

lemma CatProp4 [dest]:
"
((a::'a string) * b = c * b) ==> a = c
"
apply (insert CatProp4[ of a b c])
apply auto
done

lemma RevCat [iff]:
"
reverse (a * b) = (reverse b) * (reverse a)
"
apply (induct a b rule: cat.induct)
apply auto
done

lemma RevCat1:
"
reverse (a * b) = c ==> (reverse b) * (reverse a) = c
"
apply auto
done

lemma RevCat2:
"
 c = reverse (a * b) ==> c = (reverse b) * (reverse a)
"
apply auto
done

lemma RevStringleton [simp]:
"
reverse <x> = <x>
"
apply (simp add: Stringleton_def)
done

lemma Rev [simp]:
"
reverse (reverse a) = a
"
apply (induct a rule: reverse.induct)
apply auto
apply (simp add: CatExt)
done

lemma Rev1:
"
reverse (reverse a) = b ==> a = b
"
apply auto
done

lemma Rev2:
"
b = reverse (reverse a)  ==> b = a
"
apply auto
done


lemma RevInj [dest]:
"
reverse a = reverse b ==> a = b
"
apply (subgoal_tac "reverse (reverse a) = reverse (reverse b)")
apply (drule Rev1)
apply (drule Rev2)
apply auto
done

lemma CatProp41h:
"
(<x> * a = <x> * c ==>  a = c )
"
apply (subgoal_tac "reverse (<x> * a) = reverse (<x> * c)")
apply (drule RevCat1)
apply (drule RevCat2)
apply (drule CatProp4)
apply auto 
done

lemma CatProp41:
"
ALL a c. (b * (a::'a string) = b * c) --> a = c
"
apply (rule Axiom3)
apply clarsimp
apply (rule allI)+
apply (rule impI)+
apply (rule allI)+
apply (rule impI)+
apply (drule_tac x="<x> * aa" in spec)
apply (drule_tac x="<x> * c" in spec)
apply (simp add: CatExt)
apply (erule CatProp41h)
done

lemma CatProp41 [dest]:
"
(b * (a::'a string) = b * c) ==> a = c
"
apply (insert CatProp41[of b ])
apply auto
done

(*
lemma LengthProp3 [dest]: 
"
[|
 (a::'a string) * b = g * d;
 length b = length d
|]
==>
 b = d & a = g
"

apply (induct a b rule: cat.induct)
apply clarsimp

sorry
*)

lemma JLengthEmpty1:
"
(q = empty_string ) ==> (length q = 0)
"
apply auto
done

lemma JLengthEmpty2:
"
(length q = 0) ==> (q = empty_string )
"
apply auto
done

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


lemma JLengthEmpty3:
"
(q ~= empty_string ) ==> (length q > 0)
"
apply (erule contrapos_np)
apply (auto simp only: 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
done

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

lemma JLength [iff]:
"
length (x * y) = (length x) + (length y)
"
apply (induct x y rule: cat.induct)
apply auto
done

lemma JLengthSingleton [simp]:
"
length <x> = 1
"
apply (simp add: Stringleton_def)
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) * (y * z) = (x * y) * z
"
apply (insert semigroup_cat.add_assoc[of x y z] )
apply auto
done


function Occurs_Ct :: "'a => 'a string => nat"
where "Occurs_Ct x empty_string = 0"
      | "Occurs_Ct x (ext a y) = (if x = y then 1 + Occurs_Ct x a else Occurs_Ct x a)"
apply elim_to_cases
apply clarsimp
apply (erule contrapos_pp)
apply clarsimp
apply (drule ExNES)
apply clarsimp
apply (rule_tac x=a in exI)
apply (rule_tac x=x in exI)
apply (auto)
done

termination
apply (relation "measure (%(y,x). len(x))") 
apply auto
done

lemma OCES:
"
(ALL x. Occurs_Ct x a = 0) = (a = empty_string)
"
apply (induct a rule: Occurs_Ct.induct)
apply simp
apply auto
done

lemma OCCat:
"
Occurs_Ct x (a * c)= Occurs_Ct x a + Occurs_Ct x c
"
apply (induct a c rule: cat.induct)
apply auto
done

lemma OCLength:
"
(ALL x. Occurs_Ct x a = Occurs_Ct x b) --> length a = length b
"
apply (case_tac "a = empty_string")
apply clarsimp
apply (fold OCES)
apply clarsimp
apply (unfold OCES)
apply (drule ExNES)
apply clarsimp


sorry

lemma OCLength:
"
(ALL x. Occurs_Ct x a = Occurs_Ct x b) ==> length a = length b
"
apply (insert OCLength [of a b])
apply (drule mp)
apply auto
done

constdefs
 IsPermutation :: "'a string => 'a string => bool"
 "IsPermutation a b == (ALL x. Occurs_Ct x a = Occurs_Ct x b)"

lemma PerReflect [simp]:
"
IsPermutation a a
"
apply (unfold IsPermutation_def)
apply auto
done

lemma PerTrans [dest]:
"
[|
IsPermutation a b ;
IsPermutation b c
|]
==>
IsPermutation a c
"
apply (unfold IsPermutation_def)
apply auto
done

lemma PerCon [simp]:
"
IsPermutation (a * b) (b * a)
"
apply (unfold IsPermutation_def)
apply auto
apply (induct a b rule: cat.induct)
apply auto
apply (simp add: OCCat)
apply (simp add: OCCat)
done

lemma PerPer [dest,intro]:
"
IsPermutation a b ==> IsPermutation b a
"
apply (unfold IsPermutation_def)
apply auto
done

lemma PerCom1[intro]:
"
IsPermutation (a * b) c ==> IsPermutation (b * a) c
"
apply (simp add: IsPermutation_def)
apply (simp add: OCCat)
apply auto
apply (drule_tac x=x in spec)
apply auto
done

lemma PerCom2[intro]:
"
IsPermutation c (a * b) ==> IsPermutation c (b * a)
"
apply (simp add: IsPermutation_def)
apply (simp add: OCCat)
done

lemma PerTransIn:
"
[|
 IsPermutation (a * b) c;
 IsPermutation (d * e) a
|]
==> IsPermutation ((d * e) * b) c

"
apply (simp add: IsPermutation_def)
apply auto
apply (unfold OCCat)
apply auto
done

lemma PerComThree1:
"
  IsPermutation (a * b * c) d ==> IsPermutation (a * c * b) d
"
apply (unfold IsPermutation_def)
apply (unfold OCCat)
apply auto
apply (drule_tac x=x in spec)
apply auto
done

lemma PerComThree2:
"
  IsPermutation (a * b * c) d ==> IsPermutation (b * a * c) d
"
apply (unfold IsPermutation_def)
apply (unfold OCCat)
apply auto
apply (drule_tac x=x in spec)
apply auto
done

lemma PerComThree3:
"
  IsPermutation (a * b * c) d ==> IsPermutation (c * b * a) d
"
apply (unfold IsPermutation_def)
apply (unfold OCCat)
apply auto
apply (drule_tac x=x in spec)
apply auto
done


lemma PermCATSMT:
"
IsPermutation (a * b) c ==> length a + length b = length c
"
apply (unfold IsPermutation_def)
apply (drule OCLength)
apply auto
done

lemma PermCATSMT1:
"
IsPermutation (a * b) c ==> length a <= length c
"
apply (drule PermCATSMT)
apply (unfold length_def)
apply auto
done

lemma PermCATSMT2:
"
[|
  IsPermutation (a * b) c;
  length b > 0
|]
 ==> length a < length c
"
apply (drule PermCATSMT)
apply (unfold length_def)
apply auto
done

constdefs Is_Substring :: "'a string => 'a string => bool"
          "Is_Substring a b == (EX r s. r * a * s = b)"




lemma SS2_R [simp]:
"
Is_Substring a a
"
apply (auto simp add: Is_Substring_def)
apply (rule_tac x=empty_string in exI)+
apply auto
done

lemma SS2_T:
"
[|
 Is_Substring a b;
 Is_Substring b c
|]
==>
 Is_Substring a c
"
apply (simp add: Is_Substring_def)
apply auto
apply (rule_tac x="ra * r" in exI)
apply (rule_tac x="s * sa" in exI)
apply auto
done

lemma CatSame:
"
ALL a s. r * a * s = a --> r = empty_string
"
apply (rule Axiom3)
back
apply clarsimp
(*apply (drule CatEmpty)
apply clarsimp*)


apply (rule allI)+
apply (rule impI)+

apply (rule allI)+
apply (rule impI)+
apply (subgoal_tac "length (ext a x * aa * s) = length aa")
apply (drule LengthCat1)
apply clarsimp
apply (subgoal_tac "(String.length a + String.length s) = -1")
apply (rule_tac a="a*s" in LengthGZ1)
apply clarsimp+
done

lemma CatSame1:
"
ALL r a. r * a * s = a --> s = empty_string
"
apply (rule Axiom3)
back
apply clarsimp
(*apply (drule CatEmpty)
apply clarsimp*)


apply (rule allI)+
apply (rule impI)+

apply (rule allI)+
apply (rule impI)+
apply (subgoal_tac "length (r * aa * ext a x) = length aa")
apply (drule LengthCat1)
apply clarsimp
apply (rule_tac a="r" in LengthGZ1)
apply auto
apply (subgoal_tac "length r = -1 - length a")
apply auto
apply (unfold length_def)
apply auto
done


lemma CatSame:
"
r * a * s = a ==> s = empty_string & r = empty_string
"
apply (insert CatSame [of r])
apply (drule_tac x=a in spec)
apply (drule_tac x=s in spec)
apply (insert CatSame1 [of s])
apply (drule_tac x=r in spec)
apply (drule_tac x=a in spec)
apply auto
done

lemma CatSame11:
"
ra * r * a * s * sa = a ==> s = empty_string & r = empty_string
"
apply (insert CatSame [of "ra * r" a "s * sa"])
apply (insert CatSame1 [of "s * sa"])
apply (drule_tac x="ra *r" in spec)
apply (drule_tac x=a in spec)
apply auto
done


lemma SS2_AS:
"
[|
 Is_Substring a b;
 Is_Substring b a
|]
==> a = b
"
apply (simp add: Is_Substring_def)
apply auto
apply (drule CatSame11)
apply auto
done

lemma SSESALL [simp]:
"
Is_Substring empty_string x
"
apply (unfold Is_Substring_def)
apply auto
apply (rule_tac x=x in exI)
apply (rule_tac x=empty_string in exI)
apply auto
done


lemma SSES [intro]:
"
x ~= empty_string ==>
~ Is_Substring x empty_string
"
apply (erule contrapos_nn)
apply (auto simp add: Is_Substring_def)
(* Use older development lemmas *)
done

lemma SSExt:
"
Is_Substring a b ==> Is_Substring a (ext b x)
"
apply (unfold Is_Substring_def)
apply auto
apply (rule_tac x="r" in exI)
apply (rule_tac x="ext s x" in exI)
apply auto
done

lemma SSExtA:
"
Is_Substring (ext a x) b ==> Is_Substring a b
"
apply (unfold Is_Substring_def)
apply auto
apply (rule_tac x="r" in exI)
apply (rule_tac x="<x> * s" in exI)
apply (simp add: CatExt)
done

lemma SSExtB:
"
~ Is_Substring <y> (ext b x) ==> ~ (Is_Substring <y> b | (x = y))
"
apply (erule contrapos_nn)
apply auto
apply (erule SSExt)
apply (auto simp add: Is_Substring_def)
apply (rule_tac x=b in exI)
apply (rule_tac x=empty_string in exI)
apply auto
apply (subst CatExt)
apply auto
done

lemma SSExtC:
"
 (Is_Substring <y> b | (x = y)) ==> Is_Substring <y> (ext b x)
"
apply (erule contrapos_pp)
apply (erule SSExtB)
done

lemma SSExts1:
"
(Is_Substring <y> (ext a y))
"
apply (unfold Is_Substring_def)
apply (rule_tac x=a in exI)
apply (rule_tac x=empty_string in exI)

apply (simp add: CatExt)
done

lemma SSCat1:
"
(Is_Substring a b) ==> (Is_Substring a (c *b))
"
apply (unfold Is_Substring_def)
apply auto
apply (rule_tac x="c * r " in exI)
apply (rule_tac x="s" in exI)
apply auto
done

lemma SSCat2:
"
(Is_Substring a b) ==> (Is_Substring a (b * c))
"
apply (unfold Is_Substring_def)
apply auto
done

lemma SSCat3:
"
(Is_Substring a c) ==> (Is_Substring a (b * c))
"
apply (unfold Is_Substring_def)
apply auto
apply (rule_tac x="b * r" in exI)
apply auto
done

lemma LengthNeg:
"
length a = - length b ==> a = empty_string & b = empty_string
"
apply auto
apply (case_tac "a = empty_string")
apply auto
apply (drule ExNES)
apply auto
apply (simp add: length_def)
apply (case_tac "b = empty_string")
apply auto
apply (drule ExNES)
apply auto
apply (simp add: length_def)
done

lemma LengthNeg1:
"
length a + length b = 0 ==> a = empty_string & b = empty_string
"
apply (subgoal_tac "length a = - length b")
apply (erule LengthNeg)
apply auto
done

lemma SSExts:
"
(Is_Substring <x> <y>) = (x = y)
"
apply (unfold Is_Substring_def Stringleton_def)
apply auto
defer
apply (rule_tac x=empty_string in exI)+
apply (auto simp only: CatExt)
apply auto
apply (subgoal_tac "length (r * <x> * s) = length <y>")
apply (drule LengthCat1)+
apply auto
apply (subgoal_tac "length r = - length s")
apply auto
apply (unfold Stringleton_def)
apply auto
apply (drule LengthNeg)
apply auto
done

lemma SSExts101:
"
(Is_Substring <x>  a) = (EX y b. a = (ext b y) & (x = y | Is_Substring <x> b))
"

apply (unfold Is_Substring_def)

apply (case_tac "(EX y b. a = ext b y & (x = y | (EX r s. r * <x> * s = b)))")
apply clarsimp
apply (erule disjE)
apply (rule_tac x="b" in exI)
apply (rule_tac x="empty_string" in exI)

apply (simp add: CatExt)

apply (erule exE)+

apply (rule_tac x="r" in exI)
apply (rule_tac x="ext s y" in exI)
apply (simp add: CatExt)

apply (simp only: simp_thms)

apply simp

apply (rule allI)+

apply auto

apply (erule contrapos_pp)
apply simp

apply (case_tac "s = empty_string")
apply clarsimp
apply (rule_tac x=x in exI)
apply (rule_tac x=r in exI)
apply (simp add: CatExt)

apply (drule ExNES)
apply clarsimp
apply (rule_tac x=xa in exI)
apply (rule_tac x="(r * <x> * a)" in exI)
apply (case_tac "x = xa")
apply clarsimp+
apply (rule_tac x=r in exI)
apply (rule_tac x=a in exI)
apply clarsimp
done


lemma SSExts10:
"
(Is_Substring <x> (ext a y) & ~  (x = y )) -->(Is_Substring <x> a)
"

apply (subst SSExts101)
apply clarsimp
apply auto
done


lemma SSExts11:
"
 (Is_Substring <x> (ext a y)) --> (x = y | (Is_Substring <x> a))
"
apply (case_tac "x = y")
apply clarsimp
apply (insert SSExts10 [of x a y])
apply auto
done


lemma SSCATSTR:
"
(Is_Substring <x> (ext b y)) = ( x = y | (Is_Substring <x> b))
"
apply (subst SSExts101)
apply auto
done

lemma SSCATSTR1:
"
Is_Substring <x> (a * b) = (Is_Substring <x> a) | (Is_Substring <x> b)
"
apply (induct a b rule: cat.induct)

apply clarsimp

apply (subst SSCATSTR)
apply (simp add: SSCATSTR)
apply auto
done

lemma SSCATSTR2:
"
Is_Substring <x> (a * b) ==> (Is_Substring <x> a) | (Is_Substring <x> b)
"
apply (induct a b rule: cat.induct)

apply clarsimp

apply (subst SSCATSTR)
apply (simp add: SSCATSTR)
apply auto
done

lemma SSOC:
"
Is_Substring a b ==> (ALL x. Occurs_Ct x a <= Occurs_Ct x b)
"
apply (induct a rule: Occurs_Ct.induct)
apply clarsimp

apply clarsimp
apply (rule conjI)
apply (rule impI)
apply clarsimp
apply (frule SSExtA)
apply clarsimp
apply (case_tac "x = y")
apply clarsimp
sorry

lemma PermSS:
"
(IsPermutation a b & Is_Substring <x> a) --> Is_Substring <x> b
"

apply (unfold IsPermutation_def)

apply (rule Axiom3)
back
back
back 
back
apply (rule impI)+
apply (simp add: IsPermutation_def)
apply clarsimp
apply (simp add: Is_Substring_def)
apply clarsimp
apply (drule CatProp12)
apply clarsimp
apply (drule CatProp12)
apply clarsimp

apply (rule allI)+
apply (rule impI)+

apply simp
sorry

lemma PermSS:
"
[|IsPermutation a b ; Is_Substring <x> a|] ==> Is_Substring <x> b
"
apply (insert PermSS [of a b x])
apply auto
done

lemma PermCatSS:
"
IsPermutation (x * y) Q ==> Is_Substring x Q & Is_Substring y Q
"
sorry


constdefs URT :: "('a =>'a => bool) => 'a string => 'a string => bool"
          "URT R a b == (ALL x y. ((Is_Substring <x> a) & (Is_Substring <y> b)) --> (R x y))"


lemma SSES1 [dest]:
"
 Is_Substring x empty_string ==>
 x = empty_string
"
apply (erule contrapos_pp)
apply (erule SSES)

done

lemma URT1:
"
URT R a empty_string
"
apply (unfold URT_def)
apply auto
done

lemma URT1P [dest]:
"
URT R a empty_string ==> True
"
apply auto
done


lemma URT2:
"
URT R empty_string a
"
apply (unfold URT_def)
apply auto
done

lemma URT2P [dest]:
"
URT R empty_string a ==> True
"
apply auto
done

lemma URT3:
"
[|
 URT R a g;
 URT R b g
|]
==>
 URT R (a * b) g
"
apply (unfold URT_def)
apply auto
apply (drule_tac x=x in spec)
apply (drule_tac x=x in spec)
apply (drule_tac x=y in spec)+
apply auto
apply (drule SSCATSTR2)
apply auto
done

lemma URT3b:
"
[|
 URT R a g;
 URT R a b
|]
==>
 URT R a  (b * g)
"
apply (unfold URT_def)
apply auto
apply (drule_tac x=x in spec)
apply (drule_tac x=x in spec)
apply (drule_tac x=y in spec)+
apply (drule SSCATSTR2)
apply auto
done

lemma JURT3:
"
[|
 URT R a (ext b x)
|]
 ==> URT R a b
"
apply (unfold URT_def)
apply (rule allI)+
apply (rule impI)
apply clarify
apply (drule_tac x=xa in spec)
apply (drule_tac x=y in spec)
apply (subgoal_tac "Is_Substring <y> (ext b x)")
defer
apply (erule SSExt)
apply clarsimp
done

lemma JURT3f:
"
[|
 URT R a (ext b x)
|]
==> (ALL y. Is_Substring <y> a --> R y x)
"
apply clarify
apply (unfold URT_def)
apply (drule_tac x=y in spec)
apply (drule_tac x=x in spec)
apply (simp only: SSCATSTR)
apply simp
done

lemma JURT3g:
"
[|
 URT R a (ext b x)
|]
==>(ALL y. Is_Substring <y> a --> R y x) & URT R a b
"
apply (frule JURT3f)
apply (drule JURT3)
apply clarify
done

lemma JURT3h:
"
[|
(ALL y. Is_Substring <y> a --> R y x);
 URT R a b
|]
==>  URT R a (ext b x)
"
apply (unfold URT_def)
apply clarify
apply (simp only: SSCATSTR)

apply auto
done

lemma JURT3hc:
"
[|
(ALL y. Is_Substring <y> a --> R y x);
 URT R a b
|]
==>  URT R a ( b * <x>)
"
apply (unfold Stringleton_def)
apply auto
apply (rule JURT3h)
apply auto
apply (drule_tac x=y in spec)
apply (fold Stringleton_def)
apply auto
done


lemma JURT3i:
"
[|
(ALL y. Is_Substring <y> a --> R y x);
 URT R a b
|]
==>  URT R a (<x> * b)
"
apply (unfold URT_def)
apply clarify

apply (drule_tac x=xa in spec)
back
apply (drule_tac x=y in spec)
back

apply (case_tac "y=x")
apply clarsimp
apply (drule SSCATSTR2)
apply (simp only: SSExts)
apply auto
done



lemma JURT3P:
"
[|
  URT R a b;
  (ALL x. (Is_Substring <x> a) --> R x y)
|]
==>
 URT R a (ext b y)
"
apply (unfold URT_def)
apply clarify
apply (simp only: SSCATSTR)
apply auto
done

lemma JURT3Q:
"
[|
  URT R (ext a x) b
|]
==>
 URT R a b &   (ALL y. (Is_Substring <y> b) --> R x y)
"
apply auto
apply (unfold URT_def)
apply clarsimp
apply (drule_tac x=xa in spec)
apply (drule_tac x=y in spec)
apply (drule mp)
apply auto
apply (rule SSExtC)
apply auto
apply (drule_tac x=x in spec)
apply (drule_tac x=y in spec)
apply (drule mp)
apply auto
apply (simp add: SSExts1)
done

lemma URT4:
"
[|
 (ALL x y z. (R x y & R y z) --> R x z);
 a ~= empty_string;
 b ~= empty_string;
 c ~= empty_string
|]
==> (((URT R a b) & (URT R b c) --> (URT R a c)))
"
apply clarify

apply (unfold URT_def)
apply clarify
apply (frule ExNES)
back
apply clarify

apply (drule_tac x=x in spec)
back
apply (drule_tac x=xa in spec)
back
apply (drule_tac x=xa in spec)
back
apply (drule_tac x=y in spec)
back
apply (unfold SSCATSTR)
apply (drule_tac x=x in spec)
apply (drule_tac x=xa in spec)
apply (drule_tac x=y in spec)
apply clarsimp
done




(* Added *)


lemma URTC3:
"
[|
 (ALL x y z. (R x y & R y z) --> R x z);
  URT R <x> N;
  R y x
|]
==> URT R <y> N
"
apply (unfold  URT_def)
apply clarify
apply (unfold SSExts)
apply clarify
apply (drule_tac x=x in spec)
back
apply (drule_tac x=ya in spec)
back
apply (drule_tac x=y in spec)
apply (drule_tac x=x in spec)
apply (drule_tac x=ya in spec)
apply auto
done

lemma URT4C3:
"
URT R <x> <y> ==> R x y
"
apply (unfold URT_def)
apply (unfold SSExts)
apply auto
done

lemma URT4C4:
"
R x y ==> URT R <x> <y>
"
apply (unfold URT_def)
apply (unfold SSExts)
apply auto
done

lemma URT4C5:
"
URT R a (b * c) ==> URT R a b & URT R a c
"
apply (unfold URT_def)
apply auto
apply (drule_tac x=x in spec)
apply (drule_tac x=y in spec)
apply auto
apply (simp add: Is_Substring_def)
apply auto

apply (drule_tac x=x in spec)
apply (drule_tac x=y in spec)
apply auto
apply (simp add: Is_Substring_def)
apply auto
apply (drule_tac x="b * ra" in spec)
apply (drule_tac x="sa" in spec)
apply auto
done
(* End Add *)

lemma URT4C2:
"
[|
  (ALL x y. R x y --> ~ (R y x));
 a ~= empty_string;
 b ~= empty_string
|]
==> ((URT R a b) --> ~(URT R b a))

"
apply auto
apply (drule ExNES)+
apply auto
apply (drule JURT3Q)+
apply auto
apply (drule JURT3g)+
apply auto
apply (unfold SSCATSTR)
apply clarsimp
apply auto
done

lemma URT5P1:
"
[| 
 Is_Substring a b;
 URT R b c
|]
==>
 URT R a c

"
apply (unfold URT_def)
apply auto


apply (drule_tac x=x in spec)
apply (drule_tac x=y in spec)

apply (subgoal_tac "Is_Substring <x> b ")
apply clarify
apply (erule  SS2_T )
apply auto
done

lemma URT5P2:
"
[| 
 Is_Substring b c;
 URT R a c
|]
==>
 URT R a b
"
apply (unfold URT_def)
apply auto
apply (drule_tac x=x in spec)
apply (drule_tac x=y in spec)
apply (subgoal_tac "Is_Substring <y> c ")
apply clarify
apply (erule  SS2_T )
apply auto
done

lemma URT5P3:
"
[| 
 Is_Substring <x> c;
 URT R <min1> c
|]
==>
 R min1 x 
"
apply (unfold URT_def)
apply auto
done

lemma USRT7P1:
"
[|
 IsPermutation a b;
 URT R b c
|]
==>
 URT R a c
"
apply (unfold URT_def)

apply auto
apply (drule PermSS)
apply auto
done


lemma USRT7P2:
"
[|
 IsPermutation b c;
 URT R a b
|]
==>
 URT R a c
"
apply (unfold URT_def)
apply auto
apply (drule PerPer)


apply (drule PermSS)
apply auto
done

constdefs Is_Conformal_w :: "('a => 'a => bool)=> 'a string => bool"
        "Is_Conformal_w R b == (ALL x y. Is_Substring (<x> * <y>) b --> R x y)"

lemma Con1:
"
Is_Conformal_w R empty_string
"
apply (unfold Is_Conformal_w_def)
apply auto
apply (subgoal_tac "<x> * <y> ~= empty_string")
apply (drule SSES)
apply auto
done

lemma Con1P1:
"
Is_Conformal_w R <x>
"
apply (unfold Is_Conformal_w_def)
apply auto
apply (unfold Is_Substring_def)
apply auto
apply (subgoal_tac "length (r * <xa> * <y> * s) = length <x>")
defer
apply clarsimp
apply (unfold LengthCat)
apply auto
apply (unfold length_def)
apply auto
done

lemma Con1P2:
"
(R x y) = (Is_Conformal_w R (<x> * <y>))
"
apply (unfold Is_Conformal_w_def)
apply auto
apply (unfold Is_Substring_def)
apply (fold CatExt)
apply auto
apply (subgoal_tac "s = empty_string")
apply auto
apply (subgoal_tac "r = empty_string")
apply auto
apply (unfold Stringleton_def)
apply auto
apply (rule classical)
apply auto
apply (subgoal_tac "length (ext (ext r xa) ya * s) = length ( ext (ext empty_string x) y)")
apply (drule Length2)
apply (drule LengthCat1)
apply (auto dest:  LengthNeg1)
done

lemma Con2:
"
[|
Is_Conformal_w R b;
Is_Substring a b
|]
==> Is_Conformal_w R a
"
apply (unfold Is_Conformal_w_def)
apply auto

apply (subgoal_tac "Is_Substring (<x> * <y>) b")
apply auto
apply (erule SS2_T)
apply auto
done

lemma Con2P:
"
Is_Conformal_w R (ext a x) ==> Is_Conformal_w R a
"
apply (simp add: CatExt)
apply (rule Con2 [of R "a o <x>" a])
apply auto
apply (unfold Is_Substring_def)
apply (rule_tac x=empty_string in exI)
apply (rule_tac x="<x>" in exI)
apply auto
done

lemma Con3:
"
[|
Is_Conformal_w R (a * <x>);
Is_Conformal_w R (<x> * b)
|]
==>
Is_Conformal_w R (a * <x> * b)
"
apply (unfold Is_Conformal_w_def)
apply auto
apply (drule_tac x="xa" in spec)
apply (drule_tac x="xa" in spec)
apply (drule_tac x="y" in spec)+
apply (subgoal_tac "Is_Substring (<xa> * <y>) (a * <x>) | Is_Substring (<xa> * <y>) (<x> * b)")
apply clarify

apply clarify

apply auto
apply (unfold Is_Substring_def)
apply clarsimp
sorry

lemma Con4:
"
[|
Is_Conformal_w R (a * c);
Is_Conformal_w R (c * b)
|]
==>
Is_Conformal_w R (a * c * b)
"
apply (unfold Is_Conformal_w_def)
apply auto
sorry

lemma Con6:
"
[|
(ALL x y z. R x y & R y z --> R x z);
Is_Conformal_w R (<x> * a * <y>)
|]
==> R x y
"
apply (unfold Is_Conformal_w_def)
sorry


lemma Con7 [intro]:
"
[|
 Is_Conformal_w R (a * <x>);
 R x y
|]
==> Is_Conformal_w R (a * <x> * <y>)
"
apply (rule Con3)
apply auto
apply (unfold Con1P2)
apply auto
done

lemma Con8:
"
[|
Is_Conformal_w R a;
Is_Conformal_w R b;
URT R a b
|]
==> Is_Conformal_w R (a * b)
"
apply (unfold Is_Conformal_w_def)
apply auto
apply (unfold URT_def)
apply (drule_tac x=x in spec)
back
back
apply (drule_tac x=y in spec)
back
back
apply (drule_tac x=x in spec)
apply (drule_tac x=x in spec)
apply (drule_tac x=y in spec)+
apply auto
sorry

(* Added *)
lemma Con9:
"
[|
 URT R <x> N;
 Is_Conformal_w R N
|]
==> Is_Conformal_w R (<x> * N)
"
apply (unfold URT_def)
apply (unfold SSExts)
apply (rule Con0)
apply auto
done


lemma Con91:
"
[|
  URT R a (<x> o b);
  Is_Conformal_w R a;
  URT R <x> b
|]
==> Is_Conformal_w R (a * <x>)
"
apply (unfold Is_Conformal_w_def)
apply auto
apply (unfold URT_def)

sorry

lemma Con10:
"
[|
  Is_Conformal_w R (a * <x>);
  R x y
|]
==> Is_Conformal_w R (a * <x> * <y>)
"
sorry

 (* End Added *)

(* Hack for  Murali Code *)
context linorder
begin
abbreviation 
   LEQV :: "'a => 'a => bool"  where
  "LEQV x y ==  (x <= y)"

abbreviation 
  IsPreceding :: "'a string => 'a string => bool" where
  "IsPreceding a b == (URT less_eq a b)"

abbreviation
  IsNonDecreasing :: "'a string => bool" where
   "IsNonDecreasing a == (Is_Conformal_w less_eq a)"

end

abbreviation
  not :: "bool => bool" where
  "not b == (~ b)"

end