converted Lambda scripts;
authorwenzelm
Fri Sep 01 00:30:25 2000 +0200 (2000-09-01)
changeset 977154c6a2c6e569
parent 9770 5258ef87e85a
child 9772 c07777210a69
converted Lambda scripts;
src/HOL/IsaMakefile
src/HOL/Lambda/InductTermi.thy
src/HOL/Lambda/ListApplication.thy
src/HOL/Lambda/ListBeta.thy
src/HOL/Lambda/ListOrder.thy
src/HOL/Lambda/Type.thy
     1.1 --- a/src/HOL/IsaMakefile	Fri Sep 01 00:29:12 2000 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Fri Sep 01 00:30:25 2000 +0200
     1.3 @@ -306,8 +306,7 @@
     1.4  $(LOG)/HOL-Lambda.gz: $(OUT)/HOL Lambda/Commutation.ML \
     1.5    Lambda/Commutation.thy Lambda/Eta.ML Lambda/Eta.thy \
     1.6    Lambda/InductTermi.thy Lambda/Lambda.ML Lambda/Lambda.thy \
     1.7 -  Lambda/ListApplication.ML Lambda/ListApplication.thy \
     1.8 -  Lambda/ListBeta.thy Lambda/ListOrder.ML Lambda/ListOrder.thy \
     1.9 +  Lambda/ListApplication.thy Lambda/ListBeta.thy Lambda/ListOrder.thy \
    1.10    Lambda/ParRed.ML Lambda/ParRed.thy Lambda/Type.thy Lambda/ROOT.ML
    1.11  	@$(ISATOOL) usedir $(OUT)/HOL Lambda
    1.12  
     2.1 --- a/src/HOL/Lambda/InductTermi.thy	Fri Sep 01 00:29:12 2000 +0200
     2.2 +++ b/src/HOL/Lambda/InductTermi.thy	Fri Sep 01 00:30:25 2000 +0200
     2.3 @@ -19,7 +19,6 @@
     2.4      Var: "rs : lists IT ==> Var n $$ rs : IT"
     2.5      Lambda: "r : IT ==> Abs r : IT"
     2.6      Beta: "[| (r[s/0])$$ss : IT; s : IT |] ==> (Abs r $ s)$$ss : IT"
     2.7 -  monos lists_mono       (* FIXME move to HOL!? *)
     2.8  
     2.9  
    2.10  text {* Every term in IT terminates. *}
    2.11 @@ -34,7 +33,7 @@
    2.12    apply (erule acc_induct)
    2.13    apply clarify
    2.14    apply (rule accI)
    2.15 -  apply (tactic {* safe_tac (claset () addSEs [thm "apps_betasE"]) *})  -- FIXME
    2.16 +  apply (safe elim!: apps_betasE)
    2.17       apply assumption
    2.18      apply (blast intro: subst_preserves_beta apps_preserves_beta)
    2.19     apply (blast intro: apps_preserves_beta2 subst_preserves_beta2 rtrancl_converseI
     3.1 --- a/src/HOL/Lambda/ListApplication.thy	Fri Sep 01 00:29:12 2000 +0200
     3.2 +++ b/src/HOL/Lambda/ListApplication.thy	Fri Sep 01 00:30:25 2000 +0200
     3.3 @@ -6,9 +6,157 @@
     3.4  Application of a term to a list of terms
     3.5  *)
     3.6  
     3.7 -ListApplication = Lambda +
     3.8 +theory ListApplication = Lambda:
     3.9 +
    3.10 +syntax
    3.11 +  "_list_application" :: "dB => dB list => dB"   (infixl "$$" 150)
    3.12 +translations
    3.13 +  "t $$ ts" == "foldl (op $) t ts"
    3.14 +
    3.15 +
    3.16 +lemma apps_eq_tail_conv [iff]: "(r $$ ts = s $$ ts) = (r = s)"
    3.17 +  apply (induct_tac ts rule: rev_induct)
    3.18 +   apply auto
    3.19 +  done
    3.20 +
    3.21 +lemma Var_eq_apps_conv [rulify, iff]:
    3.22 +    "\<forall>s. (Var m = s $$ ss) = (Var m = s \<and> ss = [])"
    3.23 +  apply (induct_tac ss)
    3.24 +   apply auto
    3.25 +  done
    3.26 +
    3.27 +lemma Var_apps_eq_Var_apps_conv [rulify, iff]:
    3.28 +    "\<forall>ss. (Var m $$ rs = Var n $$ ss) = (m = n \<and> rs = ss)"
    3.29 +  apply (induct_tac rs rule: rev_induct)
    3.30 +   apply simp
    3.31 +   apply blast
    3.32 +  apply (rule allI)
    3.33 +  apply (induct_tac ss rule: rev_induct)
    3.34 +   apply auto
    3.35 +  done
    3.36 +
    3.37 +lemma App_eq_foldl_conv:
    3.38 +  "(r $ s = t $$ ts) =
    3.39 +    (if ts = [] then r $ s = t
    3.40 +    else (\<exists>ss. ts = ss @ [s] \<and> r = t $$ ss))"
    3.41 +  apply (rule_tac xs = ts in rev_exhaust)
    3.42 +   apply auto
    3.43 +  done
    3.44 +
    3.45 +lemma Abs_eq_apps_conv [iff]:
    3.46 +    "(Abs r = s $$ ss) = (Abs r = s \<and> ss = [])"
    3.47 +  apply (induct_tac ss rule: rev_induct)
    3.48 +   apply auto
    3.49 +  done
    3.50 +
    3.51 +lemma apps_eq_Abs_conv [iff]: "(s $$ ss = Abs r) = (s = Abs r \<and> ss = [])"
    3.52 +  apply (induct_tac ss rule: rev_induct)
    3.53 +   apply auto
    3.54 +  done
    3.55 +
    3.56 +lemma Abs_apps_eq_Abs_apps_conv [iff]:
    3.57 +    "\<forall>ss. (Abs r $$ rs = Abs s $$ ss) = (r = s \<and> rs = ss)"
    3.58 +  apply (induct_tac rs rule: rev_induct)
    3.59 +   apply simp
    3.60 +   apply blast
    3.61 +  apply (rule allI)
    3.62 +  apply (induct_tac ss rule: rev_induct)
    3.63 +   apply auto
    3.64 +  done
    3.65 +
    3.66 +lemma Abs_App_neq_Var_apps [iff]:
    3.67 +    "\<forall>s t. Abs s $ t ~= Var n $$ ss"
    3.68 +  apply (induct_tac ss rule: rev_induct)
    3.69 +   apply auto
    3.70 +  done
    3.71 +
    3.72 +lemma Var_apps_neq_Abs_apps [rulify, iff]:
    3.73 +    "\<forall>ts. Var n $$ ts ~= Abs r $$ ss"
    3.74 +  apply (induct_tac ss rule: rev_induct)
    3.75 +   apply simp
    3.76 +  apply (rule allI)
    3.77 +  apply (induct_tac ts rule: rev_induct)
    3.78 +   apply auto
    3.79 +  done
    3.80  
    3.81 -syntax "$$" :: dB => dB list => dB (infixl 150)
    3.82 -translations "t $$ ts" == "foldl op$ t ts"
    3.83 +lemma ex_head_tail:
    3.84 +  "\<exists>ts h. t = h $$ ts \<and> ((\<exists>n. h = Var n) \<or> (\<exists>u. h = Abs u))"
    3.85 +  apply (induct_tac t)
    3.86 +    apply (rule_tac x = "[]" in exI)
    3.87 +    apply simp
    3.88 +   apply clarify
    3.89 +   apply (rename_tac ts1 ts2 h1 h2)
    3.90 +   apply (rule_tac x = "ts1 @ [h2 $$ ts2]" in exI)
    3.91 +   apply simp
    3.92 +  apply simp
    3.93 +  done
    3.94 +
    3.95 +lemma size_apps [simp]:
    3.96 +  "size (r $$ rs) = size r + foldl (op +) 0 (map size rs) + length rs"
    3.97 +  apply (induct_tac rs rule: rev_induct)
    3.98 +   apply auto
    3.99 +  done
   3.100 +
   3.101 +lemma lem0: "[| (0::nat) < k; m <= n |] ==> m < n + k"
   3.102 +  apply simp
   3.103 +  done
   3.104 +
   3.105 +text {* A customized induction schema for @{text "$$"} *}
   3.106 +
   3.107 +lemma lem [rulify]:
   3.108 +  "[| !!n ts. \<forall>t \<in> set ts. P t ==> P (Var n $$ ts);
   3.109 +      !!u ts. [| P u; \<forall>t \<in> set ts. P t |] ==> P (Abs u $$ ts)
   3.110 +  |] ==> \<forall>t. size t = n --> P t"
   3.111 +proof -
   3.112 +  case antecedent
   3.113 +  show ?thesis
   3.114 +   apply (induct_tac n rule: less_induct)
   3.115 +   apply (rule allI)
   3.116 +   apply (cut_tac t = t in ex_head_tail)
   3.117 +   apply clarify
   3.118 +   apply (erule disjE)
   3.119 +    apply clarify
   3.120 +    apply (rule prems)
   3.121 +    apply clarify
   3.122 +    apply (erule allE, erule impE)
   3.123 +      prefer 2
   3.124 +      apply (erule allE, erule mp, rule refl)
   3.125 +     apply simp
   3.126 +     apply (rule lem0)
   3.127 +      apply force
   3.128 +     apply (rule elem_le_sum)
   3.129 +     apply force
   3.130 +    apply clarify
   3.131 +    apply (rule prems)
   3.132 +     apply (erule allE, erule impE)
   3.133 +      prefer 2
   3.134 +      apply (erule allE, erule mp, rule refl)
   3.135 +     apply simp
   3.136 +    apply clarify
   3.137 +    apply (erule allE, erule impE)
   3.138 +     prefer 2
   3.139 +     apply (erule allE, erule mp, rule refl)
   3.140 +    apply simp
   3.141 +    apply (rule le_imp_less_Suc)
   3.142 +    apply (rule trans_le_add1)
   3.143 +    apply (rule trans_le_add2)
   3.144 +    apply (rule elem_le_sum)
   3.145 +    apply force
   3.146 +    done
   3.147 +qed
   3.148 +
   3.149 +lemma Apps_dB_induct:
   3.150 +  "[| !!n ts. \<forall>t \<in> set ts. P t ==> P (Var n $$ ts);
   3.151 +      !!u ts. [| P u; \<forall>t \<in> set ts. P t |] ==> P (Abs u $$ ts)
   3.152 +  |] ==> P t"
   3.153 +proof -
   3.154 +  case antecedent
   3.155 +  show ?thesis
   3.156 +    apply (rule_tac t = t in lem)
   3.157 +      prefer 3
   3.158 +      apply (rule refl)
   3.159 +     apply (assumption | rule prems)+
   3.160 +    done
   3.161 +qed
   3.162  
   3.163  end
     4.1 --- a/src/HOL/Lambda/ListBeta.thy	Fri Sep 01 00:29:12 2000 +0200
     4.2 +++ b/src/HOL/Lambda/ListBeta.thy	Fri Sep 01 00:30:25 2000 +0200
     4.3 @@ -24,8 +24,7 @@
     4.4     apply (rule allI)
     4.5     apply (rule_tac xs = rs in rev_exhaust)
     4.6      apply simp
     4.7 -    apply (tactic {* mk_auto_tac (claset() addIs [disjI2 RS append_step1I], simpset()) 0 3 *})
     4.8 -      -- FIXME
     4.9 +    apply (auto 0 3 intro: disjI2 [THEN append_step1I])
    4.10    done
    4.11  
    4.12  
    4.13 @@ -37,9 +36,9 @@
    4.14  
    4.15  lemma apps_betasE_aux:
    4.16    "u -> u' ==> \<forall>r rs. u = r $$ rs -->
    4.17 -    ((\<exists>r'. r -> r' \<and> u' = r'$$rs) \<or>
    4.18 -     (\<exists>rs'. rs => rs' \<and> u' = r$$rs') \<or>
    4.19 -     (\<exists>s t ts. r = Abs s \<and> rs = t#ts \<and> u' = s[t/0]$$ts))"
    4.20 +    ((\<exists>r'. r -> r' \<and> u' = r' $$ rs) \<or>
    4.21 +     (\<exists>rs'. rs => rs' \<and> u' = r $$ rs') \<or>
    4.22 +     (\<exists>s t ts. r = Abs s \<and> rs = t # ts \<and> u' = s[t/0] $$ ts))"
    4.23    apply (erule beta.induct)
    4.24       apply (clarify del: disjCI)
    4.25       apply (case_tac r)
    4.26 @@ -64,8 +63,7 @@
    4.27     apply (simp only: split: split_if_asm)
    4.28      apply simp
    4.29      apply blast
    4.30 -   apply (tactic {* mk_auto_tac (claset() addIs [disjI2 RS append_step1I],simpset()) 0 3 *})
    4.31 -     -- FIXME
    4.32 +   apply (auto 0 3 intro: disjI2 [THEN append_step1I])
    4.33    done
    4.34  
    4.35  lemma apps_betasE [elim!]:
     5.1 --- a/src/HOL/Lambda/ListOrder.thy	Fri Sep 01 00:29:12 2000 +0200
     5.2 +++ b/src/HOL/Lambda/ListOrder.thy	Fri Sep 01 00:30:25 2000 +0200
     5.3 @@ -6,11 +6,111 @@
     5.4  Lifting an order to lists of elements, relating exactly one element
     5.5  *)
     5.6  
     5.7 -ListOrder = Acc +
     5.8 +theory ListOrder = Acc:
     5.9  
    5.10  constdefs
    5.11 - step1 :: "('a * 'a)set => ('a list * 'a list)set"
    5.12 -"step1 r ==
    5.13 -   {(ys,xs). ? us z z' vs. xs = us@z#vs & (z',z) : r & ys = us@z'#vs}"
    5.14 +  step1 :: "('a \<times> 'a) set => ('a list \<times> 'a list) set"
    5.15 +  "step1 r ==
    5.16 +    {(ys, xs). \<exists>us z z' vs. xs = us @ z # vs \<and> (z', z) \<in> r \<and> ys = us @ z' # vs}"
    5.17 +
    5.18 +
    5.19 +lemma step1_converse [simp]: "step1 (r^-1) = (step1 r)^-1"
    5.20 +  apply (unfold step1_def)
    5.21 +  apply blast
    5.22 +  done
    5.23 +
    5.24 +lemma in_step1_converse [iff]: "(p \<in> step1 (r^-1)) = (p \<in> (step1 r)^-1)"
    5.25 +  apply auto
    5.26 +  done
    5.27 +
    5.28 +lemma not_Nil_step1 [iff]: "([], xs) \<notin> step1 r"
    5.29 +  apply (unfold step1_def)
    5.30 +  apply blast
    5.31 +  done
    5.32 +
    5.33 +lemma not_step1_Nil [iff]: "(xs, []) \<notin> step1 r"
    5.34 +  apply (unfold step1_def)
    5.35 +  apply blast
    5.36 +  done
    5.37 +
    5.38 +lemma Cons_step1_Cons [iff]:
    5.39 +  "((y # ys, x # xs) \<in> step1 r) = ((y, x) \<in> r \<and> xs = ys \<or> x = y \<and> (ys, xs) \<in> step1 r)"
    5.40 +  apply (unfold step1_def)
    5.41 +  apply simp
    5.42 +  apply (rule iffI)
    5.43 +   apply (erule exE)
    5.44 +   apply (rename_tac ts)
    5.45 +   apply (case_tac ts)
    5.46 +    apply force
    5.47 +   apply force
    5.48 +  apply (erule disjE)
    5.49 +   apply blast
    5.50 +  apply (blast intro: Cons_eq_appendI)
    5.51 +  done
    5.52 +
    5.53 +lemma append_step1I:
    5.54 +  "(ys, xs) \<in> step1 r \<and> vs = us \<or> ys = xs \<and> (vs, us) \<in> step1 r
    5.55 +    ==> (ys @ vs, xs @ us) : step1 r"
    5.56 +  apply (unfold step1_def)
    5.57 +  apply auto
    5.58 +   apply blast
    5.59 +  apply (blast intro: append_eq_appendI)
    5.60 +  done
    5.61 +
    5.62 +lemma Cons_step1E [rulify_prems, elim!]:
    5.63 +  "[| (ys, x # xs) \<in> step1 r;
    5.64 +      \<forall>y. ys = y # xs --> (y, x) \<in> r --> R;
    5.65 +      \<forall>zs. ys = x # zs --> (zs, xs) : step1 r --> R
    5.66 +   |] ==> R"
    5.67 +  apply (case_tac ys)
    5.68 +   apply (simp add: step1_def)
    5.69 +  apply blast
    5.70 +  done
    5.71 +
    5.72 +lemma Snoc_step1_SnocD:
    5.73 +  "(ys @ [y], xs @ [x]) \<in> step1 r
    5.74 +    ==> ((ys, xs) \<in> step1 r \<and> y = x \<or> ys = xs \<and> (y, x) \<in> r)"
    5.75 +  apply (unfold step1_def)
    5.76 +  apply simp
    5.77 +  apply (clarify del: disjCI)
    5.78 +  apply (rename_tac vs)
    5.79 +  apply (rule_tac xs = vs in rev_exhaust)
    5.80 +   apply force
    5.81 +  apply simp
    5.82 +  apply blast
    5.83 +  done
    5.84 +
    5.85 +lemma Cons_acc_step1I [rulify, intro!]:
    5.86 +    "x \<in> acc r ==> \<forall>xs. xs \<in> acc (step1 r) --> x # xs \<in> acc (step1 r)"
    5.87 +  apply (erule acc_induct)
    5.88 +  apply (erule thin_rl)
    5.89 +  apply clarify
    5.90 +  apply (erule acc_induct)
    5.91 +  apply (rule accI)
    5.92 +  apply blast
    5.93 +  done
    5.94 +
    5.95 +lemma lists_accD: "xs \<in> lists (acc r) ==> xs \<in> acc (step1 r)"
    5.96 +  apply (erule lists.induct)
    5.97 +   apply (rule accI)
    5.98 +   apply simp
    5.99 +  apply (rule accI)
   5.100 +  apply (fast dest: acc_downward)
   5.101 +  done
   5.102 +
   5.103 +lemma ex_step1I: "[| x \<in> set xs; (y, x) \<in> r |]
   5.104 +    ==> \<exists>ys. (ys, xs) \<in> step1 r \<and> y \<in> set ys"
   5.105 +  apply (unfold step1_def)
   5.106 +  apply (drule in_set_conv_decomp [THEN iffD1])
   5.107 +  apply force
   5.108 +  done
   5.109 +
   5.110 +lemma lists_accI: "xs \<in> acc (step1 r) ==> xs \<in> lists (acc r)"
   5.111 +  apply (erule acc_induct)
   5.112 +  apply clarify
   5.113 +  apply (rule accI)
   5.114 +  apply (drule ex_step1I, assumption)
   5.115 +  apply blast
   5.116 +  done
   5.117  
   5.118  end
     6.1 --- a/src/HOL/Lambda/Type.thy	Fri Sep 01 00:29:12 2000 +0200
     6.2 +++ b/src/HOL/Lambda/Type.thy	Fri Sep 01 00:30:25 2000 +0200
     6.3 @@ -371,7 +371,8 @@
     6.4        apply (simp (no_asm_use))
     6.5        apply (subgoal_tac "(Var 0 $$ map (\<lambda>t. lift t 0)
     6.6          (map (\<lambda>t. t[u/i]) list))[(u $ a[u/i])/0] : IT")
     6.7 -       apply (simp (no_asm_use) del: map_compose add: map_compose [symmetric] o_def)
     6.8 +       apply (simp (no_asm_use) del: map_compose
     6.9 +	 add: map_compose [symmetric] o_def)
    6.10        apply (erule_tac x = "Ts =>> T" in allE)
    6.11        apply (erule impE)
    6.12         apply simp
    6.13 @@ -445,8 +446,9 @@
    6.14    apply (subgoal_tac "(Var 0 $ lift t 0)[s/0] : IT")
    6.15     apply simp
    6.16    apply (rule subst_type_IT)
    6.17 -  apply (rule lists.Nil [THEN 2 lists.Cons [THEN IT.Var], unfold foldl_Nil [THEN eq_reflection]
    6.18 -    foldl_Cons [THEN eq_reflection]])
    6.19 +  apply (rule lists.Nil
    6.20 +    [THEN 2 lists.Cons [THEN IT.Var], unfold foldl_Nil [THEN eq_reflection]
    6.21 +      foldl_Cons [THEN eq_reflection]])
    6.22        apply (erule lift_IT)
    6.23       apply (rule typing.App)
    6.24       apply (rule typing.Var)