# HG changeset patch
# User wenzelm
# Date 967761025 -7200
# Node ID 54c6a2c6e5690fc658f366cc317051f54c65729f
# Parent  5258ef87e85a9136a0882ee8ff3a013369f8d2b9
converted Lambda scripts;

diff -r 5258ef87e85a -r 54c6a2c6e569 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Sep 01 00:29:12 2000 +0200
+++ b/src/HOL/IsaMakefile	Fri Sep 01 00:30:25 2000 +0200
@@ -306,8 +306,7 @@
 $(LOG)/HOL-Lambda.gz: $(OUT)/HOL Lambda/Commutation.ML \
   Lambda/Commutation.thy Lambda/Eta.ML Lambda/Eta.thy \
   Lambda/InductTermi.thy Lambda/Lambda.ML Lambda/Lambda.thy \
-  Lambda/ListApplication.ML Lambda/ListApplication.thy \
-  Lambda/ListBeta.thy Lambda/ListOrder.ML Lambda/ListOrder.thy \
+  Lambda/ListApplication.thy Lambda/ListBeta.thy Lambda/ListOrder.thy \
   Lambda/ParRed.ML Lambda/ParRed.thy Lambda/Type.thy Lambda/ROOT.ML
 	@$(ISATOOL) usedir $(OUT)/HOL Lambda
 
diff -r 5258ef87e85a -r 54c6a2c6e569 src/HOL/Lambda/InductTermi.thy
--- a/src/HOL/Lambda/InductTermi.thy	Fri Sep 01 00:29:12 2000 +0200
+++ b/src/HOL/Lambda/InductTermi.thy	Fri Sep 01 00:30:25 2000 +0200
@@ -19,7 +19,6 @@
     Var: "rs : lists IT ==> Var n $$ rs : IT"
     Lambda: "r : IT ==> Abs r : IT"
     Beta: "[| (r[s/0])$$ss : IT; s : IT |] ==> (Abs r $ s)$$ss : IT"
-  monos lists_mono       (* FIXME move to HOL!? *)
 
 
 text {* Every term in IT terminates. *}
@@ -34,7 +33,7 @@
   apply (erule acc_induct)
   apply clarify
   apply (rule accI)
-  apply (tactic {* safe_tac (claset () addSEs [thm "apps_betasE"]) *})  -- FIXME
+  apply (safe elim!: apps_betasE)
      apply assumption
     apply (blast intro: subst_preserves_beta apps_preserves_beta)
    apply (blast intro: apps_preserves_beta2 subst_preserves_beta2 rtrancl_converseI
diff -r 5258ef87e85a -r 54c6a2c6e569 src/HOL/Lambda/ListApplication.thy
--- a/src/HOL/Lambda/ListApplication.thy	Fri Sep 01 00:29:12 2000 +0200
+++ b/src/HOL/Lambda/ListApplication.thy	Fri Sep 01 00:30:25 2000 +0200
@@ -6,9 +6,157 @@
 Application of a term to a list of terms
 *)
 
-ListApplication = Lambda +
+theory ListApplication = Lambda:
+
+syntax
+  "_list_application" :: "dB => dB list => dB"   (infixl "$$" 150)
+translations
+  "t $$ ts" == "foldl (op $) t ts"
+
+
+lemma apps_eq_tail_conv [iff]: "(r $$ ts = s $$ ts) = (r = s)"
+  apply (induct_tac ts rule: rev_induct)
+   apply auto
+  done
+
+lemma Var_eq_apps_conv [rulify, iff]:
+    "\<forall>s. (Var m = s $$ ss) = (Var m = s \<and> ss = [])"
+  apply (induct_tac ss)
+   apply auto
+  done
+
+lemma Var_apps_eq_Var_apps_conv [rulify, iff]:
+    "\<forall>ss. (Var m $$ rs = Var n $$ ss) = (m = n \<and> rs = ss)"
+  apply (induct_tac rs rule: rev_induct)
+   apply simp
+   apply blast
+  apply (rule allI)
+  apply (induct_tac ss rule: rev_induct)
+   apply auto
+  done
+
+lemma App_eq_foldl_conv:
+  "(r $ s = t $$ ts) =
+    (if ts = [] then r $ s = t
+    else (\<exists>ss. ts = ss @ [s] \<and> r = t $$ ss))"
+  apply (rule_tac xs = ts in rev_exhaust)
+   apply auto
+  done
+
+lemma Abs_eq_apps_conv [iff]:
+    "(Abs r = s $$ ss) = (Abs r = s \<and> ss = [])"
+  apply (induct_tac ss rule: rev_induct)
+   apply auto
+  done
+
+lemma apps_eq_Abs_conv [iff]: "(s $$ ss = Abs r) = (s = Abs r \<and> ss = [])"
+  apply (induct_tac ss rule: rev_induct)
+   apply auto
+  done
+
+lemma Abs_apps_eq_Abs_apps_conv [iff]:
+    "\<forall>ss. (Abs r $$ rs = Abs s $$ ss) = (r = s \<and> rs = ss)"
+  apply (induct_tac rs rule: rev_induct)
+   apply simp
+   apply blast
+  apply (rule allI)
+  apply (induct_tac ss rule: rev_induct)
+   apply auto
+  done
+
+lemma Abs_App_neq_Var_apps [iff]:
+    "\<forall>s t. Abs s $ t ~= Var n $$ ss"
+  apply (induct_tac ss rule: rev_induct)
+   apply auto
+  done
+
+lemma Var_apps_neq_Abs_apps [rulify, iff]:
+    "\<forall>ts. Var n $$ ts ~= Abs r $$ ss"
+  apply (induct_tac ss rule: rev_induct)
+   apply simp
+  apply (rule allI)
+  apply (induct_tac ts rule: rev_induct)
+   apply auto
+  done
 
-syntax "$$" :: dB => dB list => dB (infixl 150)
-translations "t $$ ts" == "foldl op$ t ts"
+lemma ex_head_tail:
+  "\<exists>ts h. t = h $$ ts \<and> ((\<exists>n. h = Var n) \<or> (\<exists>u. h = Abs u))"
+  apply (induct_tac t)
+    apply (rule_tac x = "[]" in exI)
+    apply simp
+   apply clarify
+   apply (rename_tac ts1 ts2 h1 h2)
+   apply (rule_tac x = "ts1 @ [h2 $$ ts2]" in exI)
+   apply simp
+  apply simp
+  done
+
+lemma size_apps [simp]:
+  "size (r $$ rs) = size r + foldl (op +) 0 (map size rs) + length rs"
+  apply (induct_tac rs rule: rev_induct)
+   apply auto
+  done
+
+lemma lem0: "[| (0::nat) < k; m <= n |] ==> m < n + k"
+  apply simp
+  done
+
+text {* A customized induction schema for @{text "$$"} *}
+
+lemma lem [rulify]:
+  "[| !!n ts. \<forall>t \<in> set ts. P t ==> P (Var n $$ ts);
+      !!u ts. [| P u; \<forall>t \<in> set ts. P t |] ==> P (Abs u $$ ts)
+  |] ==> \<forall>t. size t = n --> P t"
+proof -
+  case antecedent
+  show ?thesis
+   apply (induct_tac n rule: less_induct)
+   apply (rule allI)
+   apply (cut_tac t = t in ex_head_tail)
+   apply clarify
+   apply (erule disjE)
+    apply clarify
+    apply (rule prems)
+    apply clarify
+    apply (erule allE, erule impE)
+      prefer 2
+      apply (erule allE, erule mp, rule refl)
+     apply simp
+     apply (rule lem0)
+      apply force
+     apply (rule elem_le_sum)
+     apply force
+    apply clarify
+    apply (rule prems)
+     apply (erule allE, erule impE)
+      prefer 2
+      apply (erule allE, erule mp, rule refl)
+     apply simp
+    apply clarify
+    apply (erule allE, erule impE)
+     prefer 2
+     apply (erule allE, erule mp, rule refl)
+    apply simp
+    apply (rule le_imp_less_Suc)
+    apply (rule trans_le_add1)
+    apply (rule trans_le_add2)
+    apply (rule elem_le_sum)
+    apply force
+    done
+qed
+
+lemma Apps_dB_induct:
+  "[| !!n ts. \<forall>t \<in> set ts. P t ==> P (Var n $$ ts);
+      !!u ts. [| P u; \<forall>t \<in> set ts. P t |] ==> P (Abs u $$ ts)
+  |] ==> P t"
+proof -
+  case antecedent
+  show ?thesis
+    apply (rule_tac t = t in lem)
+      prefer 3
+      apply (rule refl)
+     apply (assumption | rule prems)+
+    done
+qed
 
 end
diff -r 5258ef87e85a -r 54c6a2c6e569 src/HOL/Lambda/ListBeta.thy
--- a/src/HOL/Lambda/ListBeta.thy	Fri Sep 01 00:29:12 2000 +0200
+++ b/src/HOL/Lambda/ListBeta.thy	Fri Sep 01 00:30:25 2000 +0200
@@ -24,8 +24,7 @@
    apply (rule allI)
    apply (rule_tac xs = rs in rev_exhaust)
     apply simp
-    apply (tactic {* mk_auto_tac (claset() addIs [disjI2 RS append_step1I], simpset()) 0 3 *})
-      -- FIXME
+    apply (auto 0 3 intro: disjI2 [THEN append_step1I])
   done
 
 
@@ -37,9 +36,9 @@
 
 lemma apps_betasE_aux:
   "u -> u' ==> \<forall>r rs. u = r $$ rs -->
-    ((\<exists>r'. r -> r' \<and> u' = r'$$rs) \<or>
-     (\<exists>rs'. rs => rs' \<and> u' = r$$rs') \<or>
-     (\<exists>s t ts. r = Abs s \<and> rs = t#ts \<and> u' = s[t/0]$$ts))"
+    ((\<exists>r'. r -> r' \<and> u' = r' $$ rs) \<or>
+     (\<exists>rs'. rs => rs' \<and> u' = r $$ rs') \<or>
+     (\<exists>s t ts. r = Abs s \<and> rs = t # ts \<and> u' = s[t/0] $$ ts))"
   apply (erule beta.induct)
      apply (clarify del: disjCI)
      apply (case_tac r)
@@ -64,8 +63,7 @@
    apply (simp only: split: split_if_asm)
     apply simp
     apply blast
-   apply (tactic {* mk_auto_tac (claset() addIs [disjI2 RS append_step1I],simpset()) 0 3 *})
-     -- FIXME
+   apply (auto 0 3 intro: disjI2 [THEN append_step1I])
   done
 
 lemma apps_betasE [elim!]:
diff -r 5258ef87e85a -r 54c6a2c6e569 src/HOL/Lambda/ListOrder.thy
--- a/src/HOL/Lambda/ListOrder.thy	Fri Sep 01 00:29:12 2000 +0200
+++ b/src/HOL/Lambda/ListOrder.thy	Fri Sep 01 00:30:25 2000 +0200
@@ -6,11 +6,111 @@
 Lifting an order to lists of elements, relating exactly one element
 *)
 
-ListOrder = Acc +
+theory ListOrder = Acc:
 
 constdefs
- step1 :: "('a * 'a)set => ('a list * 'a list)set"
-"step1 r ==
-   {(ys,xs). ? us z z' vs. xs = us@z#vs & (z',z) : r & ys = us@z'#vs}"
+  step1 :: "('a \<times> 'a) set => ('a list \<times> 'a list) set"
+  "step1 r ==
+    {(ys, xs). \<exists>us z z' vs. xs = us @ z # vs \<and> (z', z) \<in> r \<and> ys = us @ z' # vs}"
+
+
+lemma step1_converse [simp]: "step1 (r^-1) = (step1 r)^-1"
+  apply (unfold step1_def)
+  apply blast
+  done
+
+lemma in_step1_converse [iff]: "(p \<in> step1 (r^-1)) = (p \<in> (step1 r)^-1)"
+  apply auto
+  done
+
+lemma not_Nil_step1 [iff]: "([], xs) \<notin> step1 r"
+  apply (unfold step1_def)
+  apply blast
+  done
+
+lemma not_step1_Nil [iff]: "(xs, []) \<notin> step1 r"
+  apply (unfold step1_def)
+  apply blast
+  done
+
+lemma Cons_step1_Cons [iff]:
+  "((y # ys, x # xs) \<in> step1 r) = ((y, x) \<in> r \<and> xs = ys \<or> x = y \<and> (ys, xs) \<in> step1 r)"
+  apply (unfold step1_def)
+  apply simp
+  apply (rule iffI)
+   apply (erule exE)
+   apply (rename_tac ts)
+   apply (case_tac ts)
+    apply force
+   apply force
+  apply (erule disjE)
+   apply blast
+  apply (blast intro: Cons_eq_appendI)
+  done
+
+lemma append_step1I:
+  "(ys, xs) \<in> step1 r \<and> vs = us \<or> ys = xs \<and> (vs, us) \<in> step1 r
+    ==> (ys @ vs, xs @ us) : step1 r"
+  apply (unfold step1_def)
+  apply auto
+   apply blast
+  apply (blast intro: append_eq_appendI)
+  done
+
+lemma Cons_step1E [rulify_prems, elim!]:
+  "[| (ys, x # xs) \<in> step1 r;
+      \<forall>y. ys = y # xs --> (y, x) \<in> r --> R;
+      \<forall>zs. ys = x # zs --> (zs, xs) : step1 r --> R
+   |] ==> R"
+  apply (case_tac ys)
+   apply (simp add: step1_def)
+  apply blast
+  done
+
+lemma Snoc_step1_SnocD:
+  "(ys @ [y], xs @ [x]) \<in> step1 r
+    ==> ((ys, xs) \<in> step1 r \<and> y = x \<or> ys = xs \<and> (y, x) \<in> r)"
+  apply (unfold step1_def)
+  apply simp
+  apply (clarify del: disjCI)
+  apply (rename_tac vs)
+  apply (rule_tac xs = vs in rev_exhaust)
+   apply force
+  apply simp
+  apply blast
+  done
+
+lemma Cons_acc_step1I [rulify, intro!]:
+    "x \<in> acc r ==> \<forall>xs. xs \<in> acc (step1 r) --> x # xs \<in> acc (step1 r)"
+  apply (erule acc_induct)
+  apply (erule thin_rl)
+  apply clarify
+  apply (erule acc_induct)
+  apply (rule accI)
+  apply blast
+  done
+
+lemma lists_accD: "xs \<in> lists (acc r) ==> xs \<in> acc (step1 r)"
+  apply (erule lists.induct)
+   apply (rule accI)
+   apply simp
+  apply (rule accI)
+  apply (fast dest: acc_downward)
+  done
+
+lemma ex_step1I: "[| x \<in> set xs; (y, x) \<in> r |]
+    ==> \<exists>ys. (ys, xs) \<in> step1 r \<and> y \<in> set ys"
+  apply (unfold step1_def)
+  apply (drule in_set_conv_decomp [THEN iffD1])
+  apply force
+  done
+
+lemma lists_accI: "xs \<in> acc (step1 r) ==> xs \<in> lists (acc r)"
+  apply (erule acc_induct)
+  apply clarify
+  apply (rule accI)
+  apply (drule ex_step1I, assumption)
+  apply blast
+  done
 
 end
diff -r 5258ef87e85a -r 54c6a2c6e569 src/HOL/Lambda/Type.thy
--- a/src/HOL/Lambda/Type.thy	Fri Sep 01 00:29:12 2000 +0200
+++ b/src/HOL/Lambda/Type.thy	Fri Sep 01 00:30:25 2000 +0200
@@ -371,7 +371,8 @@
       apply (simp (no_asm_use))
       apply (subgoal_tac "(Var 0 $$ map (\<lambda>t. lift t 0)
         (map (\<lambda>t. t[u/i]) list))[(u $ a[u/i])/0] : IT")
-       apply (simp (no_asm_use) del: map_compose add: map_compose [symmetric] o_def)
+       apply (simp (no_asm_use) del: map_compose
+	 add: map_compose [symmetric] o_def)
       apply (erule_tac x = "Ts =>> T" in allE)
       apply (erule impE)
        apply simp
@@ -445,8 +446,9 @@
   apply (subgoal_tac "(Var 0 $ lift t 0)[s/0] : IT")
    apply simp
   apply (rule subst_type_IT)
-  apply (rule lists.Nil [THEN 2 lists.Cons [THEN IT.Var], unfold foldl_Nil [THEN eq_reflection]
-    foldl_Cons [THEN eq_reflection]])
+  apply (rule lists.Nil
+    [THEN 2 lists.Cons [THEN IT.Var], unfold foldl_Nil [THEN eq_reflection]
+      foldl_Cons [THEN eq_reflection]])
       apply (erule lift_IT)
      apply (rule typing.App)
      apply (rule typing.Var)