
diff -r d8a6b424f80a -r fa37c2a33812 Nominal/Ex/LetSimple2.thy
--- a/Nominal/Ex/LetSimple2.thy	Tue Jul 12 03:12:32 2011 +0900
+++ b/Nominal/Ex/LetSimple2.thy	Wed Jul 13 09:47:58 2011 +0100
@@ -2,6 +2,19 @@
 imports "../Nominal2" 
 begin
 
+(*
+ML {*
+   val lemma =
+     Term_XML.Encode.term #>
+     YXML.string_of_body #>
+     translate_string (fn c => if ord c < 10 then "\\00" ^ string_of_int (ord c) else c) #>
+     quote #> prefix "lemma " #>
+     Markup.markup Markup.sendback #> writeln
+*}
+
+ML {* lemma @{prop "x == x"} *}
+*)
+
 atom_decl name
 
 nominal_datatype trm =
@@ -37,20 +50,20 @@
 thm trm_assn.perm_bn_simps
 
 thm alpha_bn_raw.cases
-
+thm trm_assn.alpha_refl
+thm trm_assn.alpha_sym
+thm trm_assn.alpha_trans
 
 lemmas alpha_bn_cases[consumes 1] = alpha_bn_raw.cases[quot_lifted]
 
 lemma alpha_bn_refl: "alpha_bn x x"
-  by (induct x rule: trm_assn.inducts(2))
-     (rule TrueI, auto simp add: trm_assn.eq_iff)
+  by(rule trm_assn.alpha_refl)
+
 lemma alpha_bn_sym: "alpha_bn x y \<Longrightarrow> alpha_bn y x"
-  apply(erule alpha_bn_cases)
-  apply(auto)
-  done
+  by (rule trm_assn.alpha_sym)
 
 lemma alpha_bn_trans: "alpha_bn x y \<Longrightarrow> alpha_bn y z \<Longrightarrow> alpha_bn x z"
-  sorry
+  using trm_assn.alpha_trans by metis
 
 lemma k: "A \<Longrightarrow> A \<and> A" by blast
 
@@ -133,6 +146,9 @@
   apply(simp_all add: eqvt_at_def)
   done
 
+(* assn-function prevents automatic discharge
+termination by lexicographic_order
+*)
 
 nominal_primrec 
   subst_trm :: "trm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> trm"  ("_ [_ ::= _]" [90, 90, 90] 90) 
@@ -166,7 +182,8 @@
 
 lemma cheat: "P" sorry
 
-nominal_primrec (invariant "\<lambda>x y. case x of Inl x1 \<Rightarrow> True | Inr x2 \<Rightarrow> \<forall>p. (permute_bn p x2) = x2 \<longrightarrow> (p \<bullet> y) = y")
+nominal_primrec 
+ (invariant "\<lambda>x y. case x of Inl x1 \<Rightarrow> True | Inr x2 \<Rightarrow> \<forall>p. (permute_bn p x2) = x2 \<longrightarrow> (p \<bullet> y) = y")
     height_trm2 :: "trm \<Rightarrow> nat"
 and height_assn2 :: "assn \<Rightarrow> nat"
 where
@@ -174,7 +191,7 @@
 | "height_trm2 (App l r) = max (height_trm2 l) (height_trm2 r)"
 | "height_trm2 (Let as b) = max (height_assn2 as) (height_trm2 b)"
 | "height_assn2 (Assn x t) = (height_trm2 t)"
-  thm height_trm2_height_assn2_graph.intros
+  thm height_trm2_height_assn2_graph.intros[no_vars]
   thm height_trm2_height_assn2_graph_def
   apply (simp only: eqvt_def height_trm2_height_assn2_graph_def)
   apply (rule, perm_simp, rule)
@@ -299,14 +316,14 @@
 
 
 nominal_primrec (default "sum_case (\<lambda>x. Inl undefined) (\<lambda>x. Inr undefined)")
-  subst_trm :: "trm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> trm"  ("_ [_ ::trm= _]" [90, 90, 90] 90) and
-  subst_assn :: "assn \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> assn"  ("_ [_ ::assn= _]" [90, 90, 90] 90)
+  subst_trm2 :: "trm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> trm"  ("_ [_ ::trm2= _]" [90, 90, 90] 90) and
+  subst_assn2 :: "assn \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> assn"  ("_ [_ ::assn2= _]" [90, 90, 90] 90)
 where
-  "(Var x)[y ::trm= s] = (if x = y then s else (Var x))"
-| "(App t1 t2)[y ::trm= s] = App (t1[y ::trm= s]) (t2[y ::trm= s])"
-| "(set (bn as)) \<sharp>* (y, s) \<Longrightarrow> (Let as t)[y ::trm= s] = Let (ast[y ::assn= s]) (t[y ::trm= s])"
-| "(Assn x t)[y ::assn= s] = Assn x (t[y ::trm= s])"
-apply(subgoal_tac "\<And>p x r. subst_trm_subst_assn_graph x r \<Longrightarrow> subst_trm_subst_assn_graph (p \<bullet> x) (p \<bullet> r)")
+  "(Var x)[y ::trm2= s] = (if x = y then s else (Var x))"
+| "(App t1 t2)[y ::trm2= s] = App (t1[y ::trm2= s]) (t2[y ::trm2= s])"
+| "(set (bn as)) \<sharp>* (y, s) \<Longrightarrow> (Let as t)[y ::trm2= s] = Let (ast[y ::assn2= s]) (t[y ::trm2= s])"
+| "(Assn x t)[y ::assn2= s] = Assn x (t[y ::trm2= s])"
+apply(subgoal_tac "\<And>p x r. subst_trm2_subst_assn2_graph x r \<Longrightarrow> subst_trm2_subst_assn2_graph (p \<bullet> x) (p \<bullet> r)")
 apply(simp add: eqvt_def)
 apply(rule allI)
 apply(simp add: permute_fun_def permute_bool_def)
@@ -336,31 +353,41 @@
   apply(rule_tac y="a" in trm_assn.exhaust(2))
   apply(simp)
   apply(blast)
-  apply(simp_all)[7]
-  prefer 2
+--"compatibility" 
+  apply(all_trivials)
+  apply(simp)
   apply(simp)
   prefer 2
   apply(simp)
+  thm Inl_inject
+  apply(drule Inl_inject)
+  apply(rule arg_cong)
+  back
+  apply (simp only: meta_eq_to_obj_eq[OF subst_trm2_def, symmetric, unfolded fun_eq_iff])
+  apply (simp only: meta_eq_to_obj_eq[OF subst_assn2_def, symmetric, unfolded fun_eq_iff])
+  apply (subgoal_tac "eqvt_at (\<lambda>ast. subst_assn2 ast ya sa) ast")
+  apply (subgoal_tac "eqvt_at (\<lambda>asta. subst_assn2 asta ya sa) asta")
+  apply (subgoal_tac "eqvt_at (\<lambda>t. subst_trm2 t ya sa) t")
+  apply (subgoal_tac "eqvt_at (\<lambda>ta. subst_trm2 ta ya sa) ta")
+  apply (thin_tac "eqvt_at subst_trm2_subst_assn2_sumC (Inr (ast, y, s))")
+  apply (thin_tac "eqvt_at subst_trm2_subst_assn2_sumC (Inr (asta, ya, sa))")
+  apply (thin_tac "eqvt_at subst_trm2_subst_assn2_sumC (Inl (t, y, s))")
+  apply (thin_tac "eqvt_at subst_trm2_subst_assn2_sumC (Inl (ta, ya, sa))")
+  defer
+  apply(simp add: Abs_eq_iff alphas)
+  apply(clarify)
+  apply(rule eqvt_at_perm)
   apply(simp)
-  apply (simp only: meta_eq_to_obj_eq[OF subst_trm_def, symmetric, unfolded fun_eq_iff])
-  apply (simp only: meta_eq_to_obj_eq[OF subst_assn_def, symmetric, unfolded fun_eq_iff])
-  apply (subgoal_tac "eqvt_at (\<lambda>ast. subst_assn ast ya sa) ast")
-  apply (subgoal_tac "eqvt_at (\<lambda>asta. subst_assn asta ya sa) asta")
-  apply (subgoal_tac "eqvt_at (\<lambda>t. subst_trm t ya sa) t")
-  apply (subgoal_tac "eqvt_at (\<lambda>ta. subst_trm ta ya sa) ta")
-  apply (thin_tac "eqvt_at subst_trm_subst_assn_sumC (Inr (ast, ya, sa))")
-  apply (thin_tac "eqvt_at subst_trm_subst_assn_sumC (Inr (asta, ya, sa))")
-  apply (thin_tac "eqvt_at subst_trm_subst_assn_sumC (Inl (t, ya, sa))")
-  apply (thin_tac "eqvt_at subst_trm_subst_assn_sumC (Inl (ta, ya, sa))")
-  defer
+  apply(simp add: subst_trm2_def)
+  apply(simp add: eqvt_at_def)
   defer
   defer
   defer
   defer
   defer
   apply(rule conjI)
-  apply (subgoal_tac "subst_assn ast ya sa= subst_assn asta ya sa")
-  apply (subgoal_tac "subst_trm t ya sa = subst_trm ta ya sa")
+  apply (subgoal_tac "subst_assn2 ast ya sa= subst_assn2 asta ya sa")
+  apply (subgoal_tac "subst_trm2 t ya sa = subst_trm2 ta ya sa")
   apply(simp)
   apply(erule_tac conjE)+
   apply(erule alpha_bn_cases)




