# HG changeset patch
# User wenzelm
# Date 1280854362 -7200
# Node ID 05691ad7407976d0dca6ee46304e94f1990b49c1
# Parent  ac94ff28e9e194aacfebb17a587a4d30a7b92fce
modernized specifications;
tuned headers;

diff -r ac94ff28e9e1 -r 05691ad74079 src/HOL/Subst/AList.thy
--- 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
diff -r ac94ff28e9e1 -r 05691ad74079 src/HOL/Subst/Subst.thy
--- 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
 
diff -r ac94ff28e9e1 -r 05691ad74079 src/HOL/Subst/UTerm.thy
--- 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
diff -r ac94ff28e9e1 -r 05691ad74079 src/HOL/Subst/Unifier.thy
--- 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
diff -r ac94ff28e9e1 -r 05691ad74079 src/HOL/Subst/Unify.thy
--- 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: