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.
tuned
authorChristian Urban <urbanc@in.tum.de>
Thu, 06 Jan 2011 14:02:10 +0000
changeset 2645 09cf78bb53d4
parent 2644 8ad8612e5d9b
child 2646 51f75d24bd73
tuned
Nominal/Ex/Lambda.thy file | annotate | diff | comparison | revisions
Nominal/Ex/Weakening.thy file | annotate | diff | comparison | revisions
Nominal/nominal_inductive.ML file | annotate | diff | comparison | revisions 
--- a/Nominal/Ex/Lambda.thy	Thu Jan 06 13:31:44 2011 +0000
+++ b/Nominal/Ex/Lambda.thy	Thu Jan 06 14:02:10 2011 +0000
@@ -2,6 +2,7 @@
 imports "../Nominal2" 
 begin
 
+
 atom_decl name
 
 nominal_datatype lam =
@@ -19,161 +20,6 @@
 thm lam.fv_bn_eqvt
 thm lam.size_eqvt
 
-ML {*
-  Outer_Syntax.local_theory_to_proof;
-  Proof.theorem
-*}
-
-ML {*
-fun prove_strong_ind pred_name avoids ctxt =
-  let
-    val _ = ()
-  in
-    Proof.theorem NONE (fn thss => fn ctxt => ctxt) [] ctxt
-  end
-
-(* outer syntax *)
-local
-  structure P = Parse;
-  structure S = Scan
-
-in
-val _ =
-  Outer_Syntax.local_theory_to_proof "nominal_inductive"
-    "prove strong induction theorem for inductive predicate involving nominal datatypes"
-    Keyword.thy_goal
-    (Parse.xname -- 
-     (Scan.optional (Parse.$$$ "avoids" |-- Parse.enum1 "|" (Parse.name --
-      (Parse.$$$ ":" |-- Parse.and_list1 Parse.term))) []) >> (fn (pred_name, avoids) =>
-        prove_strong_ind pred_name avoids))
-
-end
-*}
-
-
-section {* Typing *}
-
-nominal_datatype ty =
-  TVar string
-| TFun ty ty ("_ \<rightarrow> _") 
-
-
-inductive
-  valid :: "(name \<times> ty) list \<Rightarrow> bool"
-where
-  "valid []"
-| "\<lbrakk>atom x \<sharp> Gamma; valid Gamma\<rbrakk> \<Longrightarrow> valid ((x, T)#Gamma)"
-
-inductive
-  typing :: "(name\<times>ty) list \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _ : _" [60,60,60] 60) 
-where
-    t_Var[intro]: "\<lbrakk>valid \<Gamma>; (x, T) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x : T"
-  | t_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : T1 \<rightarrow> T2; \<Gamma> \<turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : T2"
-  | t_Lam[intro]: "\<lbrakk>atom x \<sharp> \<Gamma>; (x, T1) # \<Gamma> \<turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam x t : T1 \<rightarrow> T2"
-
-equivariance valid
-equivariance typing
-
-thm valid.eqvt
-thm typing.eqvt
-thm eqvts
-thm eqvts_raw
-
-thm typing.induct[of "\<Gamma>" "t" "T", no_vars]
-
-(*
-lemma
-  fixes c::"'a::fs"
-  assumes a: "\<Gamma> \<turnstile> t : T" 
-  and a1: "\<And>\<Gamma> x T c. \<lbrakk>valid \<Gamma>; (x, T) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> P c \<Gamma> (Var x) T"
-  and a2: "\<And>\<Gamma> t1 T1 T2 t2 c. \<lbrakk>\<Gamma> \<turnstile> t1 : T1 \<rightarrow> T2; \<And>d. P d \<Gamma> t1 T1 \<rightarrow> T2; \<Gamma> \<turnstile> t2 : T1; \<And>d. P d \<Gamma> t2 T1\<rbrakk> 
-           \<Longrightarrow> P c \<Gamma> (App t1 t2) T2"
-  and a3: "\<And>x \<Gamma> T1 t T2 c. \<lbrakk>atom x \<sharp> c; atom x \<sharp> \<Gamma>; (x, T1) # \<Gamma> \<turnstile> t : T2; \<And>d. P d ((x, T1) # \<Gamma>) t T2\<rbrakk> 
-           \<Longrightarrow> P c \<Gamma> (Lam x t) T1 \<rightarrow> T2"
-  shows "P c \<Gamma> t T"
-proof -
-  from a have "\<And>p c. P c (p \<bullet> \<Gamma>) (p \<bullet> t) (p \<bullet> T)"
-  proof (induct)
-    case (t_Var \<Gamma> x T p c)
-    then show ?case
-      apply -
-      apply(perm_strict_simp)
-      apply(rule a1)
-      apply(drule_tac p="p" in permute_boolI)
-      apply(perm_strict_simp add: permute_minus_cancel)
-      apply(assumption)
-      apply(rotate_tac 1)
-      apply(drule_tac p="p" in permute_boolI)
-      apply(perm_strict_simp add: permute_minus_cancel)
-      apply(assumption)
-      done
-  next
-    case (t_App \<Gamma> t1 T1 T2 t2 p c)
-    then show ?case
-      apply -
-      apply(perm_strict_simp)
-      apply(rule a2)
-      apply(drule_tac p="p" in permute_boolI)
-      apply(perm_strict_simp add: permute_minus_cancel)
-      apply(assumption)
-      apply(assumption)
-      apply(rotate_tac 2)
-      apply(drule_tac p="p" in permute_boolI)
-      apply(perm_strict_simp add: permute_minus_cancel)
-      apply(assumption)
-      apply(assumption)
-      done
-  next
-    case (t_Lam x \<Gamma> T1 t T2 p c)
-    then show ?case
-      apply -
-      apply(subgoal_tac "\<exists>q. (q \<bullet> {p \<bullet> atom x}) \<sharp>* c \<and> 
-        supp (p \<bullet> \<Gamma>, p \<bullet> Lam x t, p \<bullet> (T1 \<rightarrow> T2)) \<sharp>* q")
-      apply(erule exE)
-      apply(rule_tac t="p \<bullet> \<Gamma>" and  s="(q + p) \<bullet> \<Gamma>" in subst)
-      apply(simp only: permute_plus)
-      apply(rule supp_perm_eq)
-      apply(simp add: supp_Pair fresh_star_union)
-      apply(rule_tac t="p \<bullet> Lam x t" and  s="(q + p) \<bullet> Lam x t" in subst)
-      apply(simp only: permute_plus)
-      apply(rule supp_perm_eq)
-      apply(simp add: supp_Pair fresh_star_union)
-      apply(rule_tac t="p \<bullet> (T1 \<rightarrow> T2)" and  s="(q + p) \<bullet> (T1 \<rightarrow> T2)" in subst)
-      apply(simp only: permute_plus)
-      apply(rule supp_perm_eq)
-      apply(simp add: supp_Pair fresh_star_union)
-      apply(simp (no_asm) only: eqvts)
-      apply(rule a3)
-      apply(simp only: eqvts permute_plus)
-      apply(simp add: fresh_star_def)
-      apply(drule_tac p="q + p" in permute_boolI)
-      apply(perm_strict_simp add: permute_minus_cancel)
-      apply(assumption)
-      apply(rotate_tac 1)
-      apply(drule_tac p="q + p" in permute_boolI)
-      apply(perm_strict_simp add: permute_minus_cancel)
-      apply(assumption)
-      apply(drule_tac x="d" in meta_spec)
-      apply(drule_tac x="q + p" in meta_spec)
-      apply(perm_strict_simp add: permute_minus_cancel)
-      apply(assumption)
-      apply(rule at_set_avoiding2)
-      apply(simp add: finite_supp)
-      apply(simp add: finite_supp)
-      apply(simp add: finite_supp)
-      apply(rule_tac p="-p" in permute_boolE)
-      apply(perm_strict_simp add: permute_minus_cancel)
-	--"supplied by the user"
-      apply(simp add: fresh_star_prod)
-      apply(simp add: fresh_star_def)
-      sorry
-  qed
-  then have "P c (0 \<bullet> \<Gamma>) (0 \<bullet> t) (0 \<bullet> T)" .
-  then show "P c \<Gamma> t T" by simp
-qed
-
-*)
-
 
 section {* Matching *}
 
--- a/Nominal/Ex/Weakening.thy	Thu Jan 06 13:31:44 2011 +0000
+++ b/Nominal/Ex/Weakening.thy	Thu Jan 06 14:02:10 2011 +0000
@@ -1,4 +1,4 @@
-theory Lambda
+theory Weakening
 imports "../Nominal2" 
 begin
 
--- a/Nominal/nominal_inductive.ML	Thu Jan 06 13:31:44 2011 +0000
+++ b/Nominal/nominal_inductive.ML	Thu Jan 06 14:02:10 2011 +0000
@@ -207,7 +207,7 @@
   by (simp add: permute_plus)}
 
 
-fun binder_tac prem intr_cvars param_trms Ps user_thm avoid avoid_trm concl_args ctxt = 
+fun binder_tac prem intr_cvars param_trms Ps user_thm avoid_trm concl_args ctxt = 
   Subgoal.FOCUS (fn {context = ctxt, params, prems, concl, ...} =>
     let
       val thy = ProofContext.theory_of ctxt
@@ -274,7 +274,7 @@
 fun case_tac ctxt Ps avoid avoid_trm intr_cvars param_trms prem user_thm concl_args =
   let
     val tac1 = non_binder_tac prem intr_cvars Ps ctxt
-    val tac2 = binder_tac prem intr_cvars param_trms Ps user_thm avoid avoid_trm concl_args ctxt
+    val tac2 = binder_tac prem intr_cvars param_trms Ps user_thm avoid_trm concl_args ctxt
   in 
     EVERY' [ rtac @{thm allI}, rtac @{thm allI}, if null avoid then tac1 else tac2 ]
   end
nominal2