--- a/src/HOL/Subst/AList.thy Tue Aug 03 18:13:57 2010 +0200
+++ b/src/HOL/Subst/AList.thy Tue Aug 03 18:52:42 2010 +0200
@@ -1,28 +1,26 @@
-(* ID: $Id$
+(* Title: HOL/Subst/AList.thy
Author: Martin Coen, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
-
*)
-header{*Association Lists*}
+header {* Association Lists *}
theory AList
imports Main
begin
-consts alist_rec :: "[('a*'b)list, 'c, ['a, 'b, ('a*'b)list, 'c]=>'c] => 'c"
-primrec
+primrec alist_rec :: "[('a*'b)list, 'c, ['a, 'b, ('a*'b)list, 'c]=>'c] => 'c"
+where
"alist_rec [] c d = c"
- "alist_rec (p # al) c d = d (fst p) (snd p) al (alist_rec al c d)"
+| "alist_rec (p # al) c d = d (fst p) (snd p) al (alist_rec al c d)"
-consts assoc :: "['a,'b,('a*'b) list] => 'b"
-primrec
+primrec assoc :: "['a,'b,('a*'b) list] => 'b"
+where
"assoc v d [] = d"
- "assoc v d (p # al) = (if v = fst p then snd p else assoc v d al)"
+| "assoc v d (p # al) = (if v = fst p then snd p else assoc v d al)"
lemma alist_induct:
- "[| P([]);
- !!x y xs. P(xs) ==> P((x,y)#xs) |] ==> P(l)"
+ "P [] \<Longrightarrow> (!!x y xs. P xs \<Longrightarrow> P ((x,y) # xs)) \<Longrightarrow> P l"
by (induct l) auto
end
--- a/src/HOL/Subst/Subst.thy Tue Aug 03 18:13:57 2010 +0200
+++ b/src/HOL/Subst/Subst.thy Tue Aug 03 18:52:42 2010 +0200
@@ -1,34 +1,36 @@
-(* Title: Subst/Subst.thy
- ID: $Id$
+(* Title: HOL/Subst/Subst.thy
Author: Martin Coen, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
*)
-header{*Substitutions on uterms*}
+header {* Substitutions on uterms *}
theory Subst
imports AList UTerm
begin
-consts
+primrec
subst :: "'a uterm => ('a * 'a uterm) list => 'a uterm" (infixl "<|" 55)
+where
+ subst_Var: "(Var v <| s) = assoc v (Var v) s"
+| subst_Const: "(Const c <| s) = Const c"
+| subst_Comb: "(Comb M N <| s) = Comb (M <| s) (N <| s)"
+
notation (xsymbols)
subst (infixl "\<lhd>" 55)
-primrec
- subst_Var: "(Var v \<lhd> s) = assoc v (Var v) s"
- subst_Const: "(Const c \<lhd> s) = Const c"
- subst_Comb: "(Comb M N \<lhd> s) = Comb (M \<lhd> s) (N \<lhd> s)"
definition
- subst_eq :: "[('a*('a uterm)) list,('a*('a uterm)) list] => bool" (infixr "=$=" 52) where
- "r =$= s \<longleftrightarrow> (\<forall>t. t \<lhd> r = t \<lhd> s)"
+ subst_eq :: "[('a*('a uterm)) list,('a*('a uterm)) list] => bool" (infixr "=$=" 52)
+ where "r =$= s \<longleftrightarrow> (\<forall>t. t \<lhd> r = t \<lhd> s)"
+
notation (xsymbols)
subst_eq (infixr "\<doteq>" 52)
definition
- comp :: "[('a*('a uterm)) list, ('a*('a uterm)) list] => ('a*('a uterm)) list"
- (infixl "<>" 56) where
- "al <> bl = alist_rec al bl (%x y xs g. (x,y \<lhd> bl)#g)"
+ comp :: "('a * 'a uterm) list \<Rightarrow> ('a * 'a uterm) list \<Rightarrow> ('a* 'a uterm) list"
+ (infixl "<>" 56)
+ where "al <> bl = alist_rec al bl (%x y xs g. (x,y \<lhd> bl) # g)"
+
notation (xsymbols)
comp (infixl "\<lozenge>" 56)
@@ -42,7 +44,7 @@
-subsection{*Basic Laws*}
+subsection {* Basic Laws *}
lemma subst_Nil [simp]: "t \<lhd> [] = t"
by (induct t) auto
@@ -54,9 +56,8 @@
apply (case_tac "t = Var v")
prefer 2
apply (erule rev_mp)+
- apply (rule_tac P =
- "%x. x \<noteq> Var v --> ~(Var v \<prec> x) --> x \<lhd> (v,t\<lhd>s) #s = x\<lhd>s"
- in uterm.induct)
+ apply (rule_tac P = "%x. x \<noteq> Var v \<longrightarrow> ~(Var v \<prec> x) \<longrightarrow> x \<lhd> (v,t\<lhd>s) #s = x\<lhd>s"
+ in uterm.induct)
apply auto
done
--- a/src/HOL/Subst/UTerm.thy Tue Aug 03 18:13:57 2010 +0200
+++ b/src/HOL/Subst/UTerm.thy Tue Aug 03 18:52:42 2010 +0200
@@ -1,52 +1,52 @@
-(* ID: $Id$
+(* Title: HOL/Subst/UTerm.thy
Author: Martin Coen, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
*)
-header{*Simple Term Structure for Unification*}
+header {* Simple Term Structure for Unification *}
theory UTerm
imports Main
begin
-text{*Binary trees with leaves that are constants or variables.*}
+text {* Binary trees with leaves that are constants or variables. *}
datatype 'a uterm =
Var 'a
| Const 'a
| Comb "'a uterm" "'a uterm"
-consts vars_of :: "'a uterm => 'a set"
-primrec
+primrec vars_of :: "'a uterm => 'a set"
+where
vars_of_Var: "vars_of (Var v) = {v}"
- vars_of_Const: "vars_of (Const c) = {}"
- vars_of_Comb: "vars_of (Comb M N) = (vars_of(M) Un vars_of(N))"
+| vars_of_Const: "vars_of (Const c) = {}"
+| vars_of_Comb: "vars_of (Comb M N) = (vars_of(M) Un vars_of(N))"
-consts occs :: "'a uterm => 'a uterm => bool" (infixl "<:" 54)
+primrec occs :: "'a uterm => 'a uterm => bool" (infixl "<:" 54)
+where
+ occs_Var: "u <: (Var v) = False"
+| occs_Const: "u <: (Const c) = False"
+| occs_Comb: "u <: (Comb M N) = (u = M | u = N | u <: M | u <: N)"
+
notation (xsymbols)
occs (infixl "\<prec>" 54)
-primrec
- occs_Var: "u \<prec> (Var v) = False"
- occs_Const: "u \<prec> (Const c) = False"
- occs_Comb: "u \<prec> (Comb M N) = (u=M | u=N | u \<prec> M | u \<prec> N)"
-consts
- uterm_size :: "'a uterm => nat"
-primrec
- uterm_size_Var: "uterm_size (Var v) = 0"
- uterm_size_Const: "uterm_size (Const c) = 0"
- uterm_size_Comb: "uterm_size (Comb M N) = Suc(uterm_size M + uterm_size N)"
+primrec uterm_size :: "'a uterm => nat"
+where
+ uterm_size_Var: "uterm_size (Var v) = 0"
+| uterm_size_Const: "uterm_size (Const c) = 0"
+| uterm_size_Comb: "uterm_size (Comb M N) = Suc(uterm_size M + uterm_size N)"
-lemma vars_var_iff: "(v \<in> vars_of(Var(w))) = (w=v)"
+lemma vars_var_iff: "(v \<in> vars_of (Var w)) = (w = v)"
by auto
-lemma vars_iff_occseq: "(x \<in> vars_of(t)) = (Var(x) \<prec> t | Var(x) = t)"
+lemma vars_iff_occseq: "(x \<in> vars_of t) = (Var x \<prec> t | Var x = t)"
by (induct t) auto
text{* Not used, but perhaps useful in other proofs *}
-lemma occs_vars_subset: "M\<prec>N \<Longrightarrow> vars_of(M) \<subseteq> vars_of(N)"
+lemma occs_vars_subset: "M \<prec> N \<Longrightarrow> vars_of M \<subseteq> vars_of N"
by (induct N) auto
@@ -54,7 +54,7 @@
"vars_of M Un vars_of N \<subseteq> (vars_of M Un A) Un (vars_of N Un B)"
by blast
-lemma finite_vars_of: "finite(vars_of M)"
+lemma finite_vars_of: "finite (vars_of M)"
by (induct M) auto
end
--- a/src/HOL/Subst/Unifier.thy Tue Aug 03 18:13:57 2010 +0200
+++ b/src/HOL/Subst/Unifier.thy Tue Aug 03 18:52:42 2010 +0200
@@ -1,26 +1,26 @@
-(* ID: $Id$
+(* Title: HOL/Subst/Unifier.thy
Author: Martin Coen, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
*)
-header{*Definition of Most General Unifier*}
+header {* Definition of Most General Unifier *}
theory Unifier
imports Subst
begin
definition
- Unifier :: "[('a * 'a uterm)list, 'a uterm, 'a uterm] => bool" where
- "Unifier s t u \<longleftrightarrow> t <| s = u <| s"
+ Unifier :: "('a * 'a uterm) list \<Rightarrow> 'a uterm \<Rightarrow> 'a uterm \<Rightarrow> bool"
+ where "Unifier s t u \<longleftrightarrow> t <| s = u <| s"
definition
- MoreGeneral :: "[('a * 'a uterm)list, ('a * 'a uterm)list] => bool" (infixr ">>" 52) where
- "r >> s \<longleftrightarrow> (\<exists>q. s =$= r <> q)"
+ MoreGeneral :: "('a * 'a uterm) list \<Rightarrow> ('a * 'a uterm) list \<Rightarrow> bool" (infixr ">>" 52)
+ where "r >> s \<longleftrightarrow> (\<exists>q. s =$= r <> q)"
definition
- MGUnifier :: "[('a * 'a uterm)list, 'a uterm, 'a uterm] => bool" where
- "MGUnifier s t u \<longleftrightarrow> Unifier s t u & (\<forall>r. Unifier r t u --> s >> r)"
+ MGUnifier :: "('a * 'a uterm) list \<Rightarrow> 'a uterm \<Rightarrow> 'a uterm \<Rightarrow> bool"
+ where "MGUnifier s t u \<longleftrightarrow> Unifier s t u & (\<forall>r. Unifier r t u --> s >> r)"
definition
Idem :: "('a * 'a uterm)list => bool" where
@@ -30,17 +30,17 @@
lemmas unify_defs = Unifier_def MoreGeneral_def MGUnifier_def
-subsection{*Unifiers*}
+subsection {* Unifiers *}
lemma Unifier_Comb [iff]: "Unifier s (Comb t u) (Comb v w) = (Unifier s t v & Unifier s u w)"
by (simp add: Unifier_def)
-lemma Cons_Unifier: "[| v ~: vars_of t; v ~: vars_of u; Unifier s t u |] ==> Unifier ((v,r)#s) t u"
+lemma Cons_Unifier: "v \<notin> vars_of t \<Longrightarrow> v \<notin> vars_of u \<Longrightarrow> Unifier s t u \<Longrightarrow> Unifier ((v, r) #s) t u"
by (simp add: Unifier_def repl_invariance)
-subsection{* Most General Unifiers*}
+subsection {* Most General Unifiers *}
lemma mgu_sym: "MGUnifier s t u = MGUnifier s u t"
by (simp add: unify_defs eq_commute)
@@ -64,26 +64,26 @@
done
-subsection{*Idempotence*}
+subsection {* Idempotence *}
-lemma Idem_Nil [iff]: "Idem([])"
+lemma Idem_Nil [iff]: "Idem []"
by (simp add: Idem_def)
-lemma Idem_iff: "Idem(s) = (sdom(s) Int srange(s) = {})"
+lemma Idem_iff: "Idem s = (sdom s Int srange s = {})"
by (simp add: Idem_def subst_eq_iff invariance dom_range_disjoint)
-lemma Var_Idem [intro!]: "~ (Var(v) <: t) ==> Idem([(v,t)])"
+lemma Var_Idem [intro!]: "~ (Var v <: t) ==> Idem [(v,t)]"
by (simp add: vars_iff_occseq Idem_iff srange_iff empty_iff_all_not)
lemma Unifier_Idem_subst:
- "[| Idem(r); Unifier s (t<|r) (u<|r) |]
- ==> Unifier (r <> s) (t <| r) (u <| r)"
+ "Idem(r) \<Longrightarrow> Unifier s (t<|r) (u<|r) \<Longrightarrow>
+ Unifier (r <> s) (t <| r) (u <| r)"
by (simp add: Idem_def Unifier_def comp_subst_subst)
lemma Idem_comp:
- "[| Idem(r); Unifier s (t <| r) (u <| r);
- !!q. Unifier q (t <| r) (u <| r) ==> s <> q =$= q
- |] ==> Idem(r <> s)"
+ "Idem r \<Longrightarrow> Unifier s (t <| r) (u <| r) \<Longrightarrow>
+ (!!q. Unifier q (t <| r) (u <| r) \<Longrightarrow> s <> q =$= q) \<Longrightarrow>
+ Idem (r <> s)"
apply (frule Unifier_Idem_subst, blast)
apply (force simp add: Idem_def subst_eq_iff)
done
--- a/src/HOL/Subst/Unify.thy Tue Aug 03 18:13:57 2010 +0200
+++ b/src/HOL/Subst/Unify.thy Tue Aug 03 18:52:42 2010 +0200
@@ -1,10 +1,9 @@
-(* ID: $Id$
+(* Title: HOL/Subst/Unify.thy
Author: Konrad Slind, Cambridge University Computer Laboratory
Copyright 1997 University of Cambridge
-
*)
-header{*Unification Algorithm*}
+header {* Unification Algorithm *}
theory Unify
imports Unifier
@@ -27,7 +26,7 @@
*}
definition
- unifyRel :: "(('a uterm * 'a uterm) * ('a uterm * 'a uterm)) set" where
+ unifyRel :: "(('a uterm * 'a uterm) * ('a uterm * 'a uterm)) set" where
"unifyRel = inv_image (finite_psubset <*lex*> measure uterm_size)
(%(M,N). (vars_of M Un vars_of N, M))"
--{*Termination relation for the Unify function: