Mercurial Mercurial > hg > nominal2 / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
slight tuning
authorChristian Urban <urbanc@in.tum.de>
Wed, 13 Jul 2011 09:47:58 +0100
changeset 2966 fa37c2a33812
parent 2965 d8a6b424f80a
child 2967 d7e8b9b78e28
slight tuning
Nominal/Ex/LetSimple2.thy file | annotate | diff | comparison | revisions
Nominal/Nominal2.thy file | annotate | diff | comparison | revisions 
--- 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)
--- a/Nominal/Nominal2.thy	Tue Jul 12 03:12:32 2011 +0900
+++ b/Nominal/Nominal2.thy	Wed Jul 13 09:47:58 2011 +0100
@@ -328,7 +328,7 @@
   val alpha_bn_rsp = 
     raw_alpha_bn_rsp alpha_result alpha_bn_equivp_thms alpha_bn_imp_thms
 
-  val raw_perm_bn_rsp =raw_perm_bn_rsp lthy5 alpha_result raw_perm_bns raw_perm_bn_simps
+  val raw_perm_bn_rsp = raw_perm_bn_rsp lthy5 alpha_result raw_perm_bns raw_perm_bn_simps
 
   (* noting the quot_respects lemmas *)
   val (_, lthy6) = 
@@ -408,7 +408,7 @@
 
   val ([ qdistincts, qeq_iffs, qfv_defs, qbn_defs, qperm_simps, qfv_qbn_eqvts, 
          qbn_inducts, qsize_eqvt, [qinduct], qexhausts, qsize_simps, qperm_bn_simps, 
-         qalpha_refl_thms ], lthyB) = 
+         qalpha_refl_thms, qalpha_sym_thms, qalpha_trans_thms ], lthyB) = 
     lthy9a    
     |>>> lift_thms qtys [] alpha_distincts  
     ||>>> lift_thms qtys eq_iff_simps alpha_eq_iff       
@@ -423,6 +423,8 @@
     ||>>> lift_thms qtys [] raw_size_thms
     ||>>> lift_thms qtys [] raw_perm_bn_simps
     ||>>> lift_thms qtys [] alpha_refl_thms
+    ||>>> lift_thms qtys [] alpha_sym_thms
+    ||>>> lift_thms qtys [] alpha_trans_thms
 
   val qinducts = Project_Rule.projections lthyB qinduct
 
@@ -512,6 +514,10 @@
      ||>> Local_Theory.note ((thms_suffix "bn_finite", []), qbn_finite_thms)
      ||>> Local_Theory.note ((thms_suffix "perm_bn_alpha", []), qperm_bn_alpha_thms)
      ||>> Local_Theory.note ((thms_suffix "permute_bn", []), qpermute_bn_thms)
+     ||>> Local_Theory.note ((thms_suffix "alpha_refl", []), qalpha_refl_thms)
+     ||>> Local_Theory.note ((thms_suffix "alpha_sym", []), qalpha_sym_thms)
+     ||>> Local_Theory.note ((thms_suffix "alpha_trans", []), qalpha_trans_thms)
+     
 in
   lthy9'
 end
nominal2