src/HOL/Lambda/ListBeta.thy

--- a/src/HOL/Lambda/ListBeta.thy	Thu Aug 31 00:16:32 2000 +0200
+++ b/src/HOL/Lambda/ListBeta.thy	Thu Aug 31 01:42:23 2000 +0200
@@ -6,9 +6,106 @@
 Lifting beta-reduction to lists of terms, reducing exactly one element
 *)
 
-ListBeta = ListApplication + ListOrder +
+theory ListBeta = ListApplication + ListOrder:
+
+syntax
+  "_list_beta" :: "dB => dB => bool"   (infixl "=>" 50)
+translations
+  "rs => ss" == "(rs,ss) : step1 beta"
+
+lemma head_Var_reduction_aux:
+  "v -> v' ==> \<forall>rs. v = Var n $$ rs --> (\<exists>ss. rs => ss \<and> v' = Var n $$ ss)"
+  apply (erule beta.induct)
+     apply simp
+    apply (rule allI)
+    apply (rule_tac xs = rs in rev_exhaust)
+     apply simp
+    apply (force intro: append_step1I)
+   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
+  done
+
+
+lemma head_Var_reduction:
+  "Var n $$ rs -> v ==> (\<exists>ss. rs => ss \<and> v = Var n $$ ss)"
+  apply (drule head_Var_reduction_aux)
+  apply blast
+  done
 
-syntax "=>" :: dB => dB => bool (infixl 50)
-translations "rs => ss" == "(rs,ss) : step1 beta"
+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))"
+  apply (erule beta.induct)
+     apply (clarify del: disjCI)
+     apply (case_tac r)
+       apply simp
+      apply (simp add: App_eq_foldl_conv)
+      apply (simp only: split: split_if_asm)
+       apply simp
+       apply blast
+      apply simp
+     apply (simp add: App_eq_foldl_conv)
+     apply (simp only: split: split_if_asm)
+      apply simp
+     apply simp
+    apply (clarify del: disjCI)
+    apply (drule App_eq_foldl_conv [THEN iffD1])
+    apply (simp only: split: split_if_asm)
+     apply simp
+     apply blast
+    apply (force intro: disjI1 [THEN append_step1I])
+   apply (clarify del: disjCI)
+   apply (drule App_eq_foldl_conv [THEN iffD1])
+   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
+  done
+
+lemma apps_betasE [elim!]:
+"[| r $$ rs -> s; !!r'. [| r -> r'; s = r' $$ rs |] ==> R;
+        !!rs'. [| rs => rs'; s = r $$ rs' |] ==> R;
+        !!t u us. [| r = Abs t; rs = u # us; s = t[u/0] $$ us |] ==> R |]
+     ==> R"
+proof -
+  assume major: "r $$ rs -> s"
+  case antecedent
+  show ?thesis
+    apply (cut_tac major [THEN apps_betasE_aux, THEN spec, THEN spec])
+    apply (assumption | rule refl | erule prems exE conjE impE disjE)+
+    done
+qed
+
+lemma apps_preserves_beta [simp]:
+    "r -> s ==> r $$ ss -> s $$ ss"
+  apply (induct_tac ss rule: rev_induct)
+  apply auto
+  done
+
+lemma apps_preserves_beta2 [simp]:
+    "r ->> s ==> r $$ ss ->> s $$ ss"
+  apply (erule rtrancl_induct)
+   apply blast
+  apply (blast intro: apps_preserves_beta rtrancl_into_rtrancl)
+  done
+
+lemma apps_preserves_betas [rulify, simp]:
+  "\<forall>ss. rs => ss --> r $$ rs -> r $$ ss"
+  apply (induct_tac rs rule: rev_induct)
+   apply simp
+  apply simp
+  apply clarify
+  apply (rule_tac xs = ss in rev_exhaust)
+   apply simp
+  apply simp
+  apply (drule Snoc_step1_SnocD)
+  apply blast
+  done
 
 end