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.
Reorder constructors to match Lambda
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Wed, 21 Dec 2011 17:05:00 +0900
changeset 3089 9bcf02a6eea9
parent 3088 5e74bd87bcda
child 3090 19f5e7afad89
child 3092 ff377f9d030a
Reorder constructors to match Lambda
Nominal/Ex/CPS/CPS1_Plotkin.thy file | annotate | diff | comparison | revisions
Nominal/Ex/CPS/CPS2_DanvyNielsen.thy file | annotate | diff | comparison | revisions
Nominal/Ex/CPS/CPS3_DanvyFilinski.thy file | annotate | diff | comparison | revisions
Nominal/Ex/CPS/Lt.thy file | annotate | diff | comparison | revisions 
--- a/Nominal/Ex/CPS/CPS1_Plotkin.thy	Wed Dec 21 15:47:42 2011 +0900
+++ b/Nominal/Ex/CPS/CPS1_Plotkin.thy	Wed Dec 21 17:05:00 2011 +0900
@@ -17,12 +17,12 @@
 apply (auto)
 apply (rule_tac x="name" and ?'a="name" in obtain_fresh)
 apply (simp_all add: fresh_at_base)[3]
-apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh)
-apply (simp add: fresh_Pair_elim fresh_at_base)[2]
 apply (rule_tac x="(lt1, lt2)" and ?'a="name" in obtain_fresh)
 apply (rule_tac x="(lt2, a)" and ?'a="name" in obtain_fresh)
 apply (rule_tac x="(a, aa)" and ?'a="name" in obtain_fresh)
 apply (simp add: fresh_Pair_elim fresh_at_base)
+apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh)
+apply (simp add: fresh_Pair_elim fresh_at_base)[2]
 apply (simp add: Abs1_eq_iff lt.fresh fresh_at_base)
 --"-"
 apply(rule_tac s="[[atom ka]]lst. ka~ $ Lam x (CPS_sumC M)" in trans)
@@ -30,7 +30,7 @@
 apply simp
 apply(simp (no_asm) add: Abs1_eq_iff del:eqvts)
 apply (simp del: eqvts add: lt.fresh fresh_at_base)
-apply (simp only: lt.perm_simps(1) lt.perm_simps(3) flip_def[symmetric] lt.eq_iff(3))
+apply (simp only: lt.perm_simps(1) lt.perm_simps(2) flip_def[symmetric] lt.eq_iff)
 apply (subst  flip_at_base_simps(2))
 apply simp
 apply (intro conjI refl)
--- a/Nominal/Ex/CPS/CPS2_DanvyNielsen.thy	Wed Dec 21 15:47:42 2011 +0900
+++ b/Nominal/Ex/CPS/CPS2_DanvyNielsen.thy	Wed Dec 21 17:05:00 2011 +0900
@@ -74,19 +74,20 @@
   apply (case_tac x)
   apply (rule_tac y="a" in lt.exhaust)
   apply auto
+  apply blast
   apply (rule_tac x="lt" and ?'a="name" in obtain_fresh)
   apply (simp add: Abs1_eq_iff)
   apply blast+
   apply (rule_tac y="b" in lt.exhaust)
   apply auto
-  apply (rule_tac x="lt" and ?'a="name" in obtain_fresh)
-  apply (simp add: Abs1_eq_iff)
-  apply blast
   apply (rule_tac ?'a="name" in obtain_fresh)
   apply (rule_tac x="(lt1, lt2, a)" and ?'a="name" in obtain_fresh)
   apply (simp add: fresh_Pair_elim)
   apply (case_tac "isValue lt1", case_tac [!] "isValue lt2")[1]
   apply (simp_all add: fresh_Pair)[4]
+  apply (rule_tac x="lt" and ?'a="name" in obtain_fresh)
+  apply (simp add: Abs1_eq_iff)
+  apply blast
 --""
   apply (rule_tac x="(y, ya, b, ba, M, Ma)" and ?'a="name" in obtain_fresh)
   apply (subgoal_tac "Lam b (Sum_Type.Projr (CPSv_CPS_sumC (Inr M))<(b~)>) = Lam a (Sum_Type.Projr (CPSv_CPS_sumC (Inr M))<(a~)>)")
--- a/Nominal/Ex/CPS/CPS3_DanvyFilinski.thy	Wed Dec 21 15:47:42 2011 +0900
+++ b/Nominal/Ex/CPS/CPS3_DanvyFilinski.thy	Wed Dec 21 17:05:00 2011 +0900
@@ -26,10 +26,9 @@
   apply (case_tac b)
   apply (rule_tac y="a" in lt.strong_exhaust)
   apply auto[3]
-  apply blast
+  apply blast+
   apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh) 
   apply (simp add: fresh_at_base Abs1_eq_iff)
-  apply blast
 --"-"
   apply (subgoal_tac "Lam c (ka (c~)) = Lam ca (ka (ca~))")
   apply (simp only:)
--- a/Nominal/Ex/CPS/Lt.thy	Wed Dec 21 15:47:42 2011 +0900
+++ b/Nominal/Ex/CPS/Lt.thy	Wed Dec 21 17:05:00 2011 +0900
@@ -7,8 +7,8 @@
 
 nominal_datatype lt =
     Var name       ("_~"  [150] 149)
+  | App lt lt         (infixl "$" 100)
   | Lam x::"name" t::"lt"  binds  x in t
-  | App lt lt         (infixl "$" 100)
 
 nominal_primrec
   subst :: "lt \<Rightarrow> name \<Rightarrow> lt \<Rightarrow> lt"  ("_ [_ ::= _]" [90, 90, 90] 90)
nominal2