LamEx.thy
changeset 259 22c199522bef
parent 258 93ea455b29f1
child 265 5f3b364d4765
equal deleted inserted replaced
258:93ea455b29f1 259:22c199522bef
     9 nominal_datatype rlam =
     9 nominal_datatype rlam =
    10   rVar "name"
    10   rVar "name"
    11 | rApp "rlam" "rlam"
    11 | rApp "rlam" "rlam"
    12 | rLam "name" "rlam"
    12 | rLam "name" "rlam"
    13 
    13 
       
    14 print_theorems
    14 
    15 
    15 function
    16 function
    16   rfv :: "rlam \<Rightarrow> name set"
    17   rfv :: "rlam \<Rightarrow> name set"
    17 where
    18 where
    18   rfv_var: "rfv (rVar a) = {a}"
    19   rfv_var: "rfv (rVar a) = {a}"
    26   alpha :: "rlam \<Rightarrow> rlam \<Rightarrow> bool" ("_ \<approx> _" [100, 100] 100)
    27   alpha :: "rlam \<Rightarrow> rlam \<Rightarrow> bool" ("_ \<approx> _" [100, 100] 100)
    27 where
    28 where
    28   a1: "a = b \<Longrightarrow> (rVar a) \<approx> (rVar b)"
    29   a1: "a = b \<Longrightarrow> (rVar a) \<approx> (rVar b)"
    29 | a2: "\<lbrakk>t1 \<approx> t2; s1 \<approx> s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx> rApp t2 s2"
    30 | a2: "\<lbrakk>t1 \<approx> t2; s1 \<approx> s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx> rApp t2 s2"
    30 | a3: "\<lbrakk>t \<approx> ([(a,b)]\<bullet>s); a \<notin> rfv (rLam b t)\<rbrakk> \<Longrightarrow> rLam a t \<approx> rLam b s"
    31 | a3: "\<lbrakk>t \<approx> ([(a,b)]\<bullet>s); a \<notin> rfv (rLam b t)\<rbrakk> \<Longrightarrow> rLam a t \<approx> rLam b s"
       
    32 
       
    33 print_theorems
    31 
    34 
    32 quotient lam = rlam / alpha
    35 quotient lam = rlam / alpha
    33 sorry
    36 sorry
    34 
    37 
    35 print_quotients
    38 print_quotients
   174 ML {* val fv_var = lift_thm_lam @{context} @{thm rfv_var} *}
   177 ML {* val fv_var = lift_thm_lam @{context} @{thm rfv_var} *}
   175 ML {* val fv_app = lift_thm_lam @{context} @{thm rfv_app} *}
   178 ML {* val fv_app = lift_thm_lam @{context} @{thm rfv_app} *}
   176 ML {* val fv_lam = lift_thm_lam @{context} @{thm rfv_lam} *}
   179 ML {* val fv_lam = lift_thm_lam @{context} @{thm rfv_lam} *}
   177 
   180 
   178 ML {* val a1 = lift_thm_lam @{context} @{thm a1} *}
   181 ML {* val a1 = lift_thm_lam @{context} @{thm a1} *}
   179 ML {* val a2 = lift_thm_lam @{context} @{thm a1} *}
   182 ML {* val a2 = lift_thm_lam @{context} @{thm a2} *}
   180 ML {* val a3 = lift_thm_lam @{context} @{thm a3} *}
   183 ML {* val a3 = lift_thm_lam @{context} @{thm a3} *}
   181 
   184 
   182 ML {* val alpha_cases = lift_thm_lam @{context} @{thm alpha.cases} *}
   185 ML {* val alpha_cases = lift_thm_lam @{context} @{thm alpha.cases} *}
   183 
   186 
   184 local_setup {*
   187 local_setup {*
   238       (rtac @{thm RIGHT_RES_FORALL_REGULAR})
   241       (rtac @{thm RIGHT_RES_FORALL_REGULAR})
   239      ]);
   242      ]);
   240  *}
   243  *}
   241   apply (tactic {* tac @{context} 1 *}) *)
   244   apply (tactic {* tac @{context} 1 *}) *)
   242 ML {* val t_r = regularize t_a rty rel rel_eqv rel_refl @{context} *}
   245 ML {* val t_r = regularize t_a rty rel rel_eqv rel_refl @{context} *}
       
   246 
   243 (*ML {*
   247 (*ML {*
   244   val rt = build_repabs_term @{context} t_r consts rty qty
   248   val rt = build_repabs_term @{context} t_r consts rty qty
   245   val rg = Logic.mk_equals ((Thm.prop_of t_r), rt);
   249   val rg = Logic.mk_equals ((Thm.prop_of t_r), rt);
   246 *}
   250 *}
   247 prove rg
   251 prove rg
   277 
   281 
   278 ML {* val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms *}
   282 ML {* val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms *}
   279 
   283 
   280 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm alpha.induct})) *}
   284 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm alpha.induct})) *}
   281 ML {* val aps = findaps rty (prop_of (atomize_thm @{thm alpha.induct})) *}
   285 ML {* val aps = findaps rty (prop_of (atomize_thm @{thm alpha.induct})) *}
   282 
       
   283 ML {*
       
   284 
       
   285 
       
   286 *}
       
   287 
       
   288 ML {* val aps = @{typ "LamEx.rlam \<Rightarrow> bool"} :: aps; *}
   286 ML {* val aps = @{typ "LamEx.rlam \<Rightarrow> bool"} :: aps; *}
       
   287 ML {* val thm = 
       
   288   @{thm FORALL_PRS[OF FUN_QUOTIENT[OF QUOTIENT_lam FUN_QUOTIENT[OF QUOTIENT_lam IDENTITY_QUOTIENT]]]} *}
       
   289 ML {* val t_a = simp_allex_prs quot [thm] t_t *}
   289 ML {* val simp_app_prs_thms = map (make_simp_prs_thm @{context} quot @{thm APP_PRS}) aps *}
   290 ML {* val simp_app_prs_thms = map (make_simp_prs_thm @{context} quot @{thm APP_PRS}) aps *}
   290 ML {* val simp_lam_prs_thms = map (make_simp_prs_thm @{context} quot @{thm LAMBDA_PRS}) abs *}
   291 ML {* val simp_lam_prs_thms = map (make_simp_prs_thm @{context} quot @{thm LAMBDA_PRS}) abs *}
   291 ML {* val t_l = repeat_eqsubst_thm @{context} (simp_app_prs_thms @ simp_lam_prs_thms) t_t *}
   292 
   292 ML {* val t_a = simp_allex_prs @{context} quot t_l *}
   293 ML {* val t_l = repeat_eqsubst_thm @{context} (simp_app_prs_thms @  simp_lam_prs_thms) t_a *}
   293 ML {* val thm = 
       
   294   @{thm FORALL_PRS[OF FUN_QUOTIENT[OF QUOTIENT_lam FUN_QUOTIENT[OF QUOTIENT_lam IDENTITY_QUOTIENT]], symmetric]} *}
       
   295 ML {* val t_a1 = eqsubst_thm @{context} [thm] t_a *}
       
   296 ML {* val defs_sym = add_lower_defs @{context} defs; *}
   294 ML {* val defs_sym = add_lower_defs @{context} defs; *}
   297 ML {* val t_d = repeat_eqsubst_thm @{context} defs_sym t_a1 *}
   295 ML {* val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym *}
       
   296 ML t_l
       
   297 ML {* val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_l *}
       
   298 ML {* val t_d = repeat_eqsubst_thm @{context} defs_sym t_d0 *}
   298 ML {* val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d *}
   299 ML {* val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d *}
   299 ML {* val t_r1 = repeat_eqsubst_thm @{context} @{thms fun_map.simps} t_r *}
   300 ML {* val t_r1 = repeat_eqsubst_thm @{context} @{thms fun_map.simps} t_r *}
   300 ML {* val t_r2 = repeat_eqsubst_thm @{context} @{thms QUOT_TYPE_I_lam.thm10} t_r1 *}
   301 ML {* val t_r2 = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_lam.thm10} t_r1 *}
   301 ML {* val t_r3 = repeat_eqsubst_thm @{context} @{thms id_apply} t_r2 *}
   302 ML {* val t_r3 = MetaSimplifier.rewrite_rule @{thms eq_reflection[OF id_apply]} t_r2 *}
   302 
       
   303 ML {* val alpha_induct = ObjectLogic.rulify t_r3 *}
   303 ML {* val alpha_induct = ObjectLogic.rulify t_r3 *}
   304 
   304 
   305 local_setup {*
   305 local_setup {*
   306   Quotient.note (@{binding "alpha_induct"}, alpha_induct) #> snd
   306   Quotient.note (@{binding "alpha_induct"}, alpha_induct) #> snd
   307 *}
   307 *}
   308 
   308 
       
   309 thm alpha_induct
       
   310 thm alpha.induct
       
   311 
       
   312 lemma rvar_inject: "rVar a \<approx> rVar b \<Longrightarrow> (a = b)"
       
   313 apply (rule alpha.cases)
       
   314 apply (assumption)
       
   315 apply (assumption)
       
   316 apply (simp_all)
       
   317 apply (cases "a = b")
       
   318 apply (simp_all)
       
   319 apply (cases "ba = b")
       
   320 apply (simp_all)
       
   321 
       
   322 
       
   323 lemma var_inject_test:
       
   324   fixes a b
       
   325   assumes a: "Var a = Var b"
       
   326   shows "(a = b)"
       
   327   using a   apply (cases "a = b")
       
   328   apply (simp_all)
       
   329   apply (rule_tac x="Var a" and xa = "Var b" in alpha_cases)
       
   330   apply (rule a)
       
   331 
       
   332 
   309 lemma
   333 lemma
   310   assumes a: "(a::lam) = b"
   334   assumes a: "(x::lam) = y"
   311   shows "False"
   335   shows "P x y"
   312   using a
   336   apply (induct rule: alpha_induct)
   313   apply (rule alpha_induct)
   337   apply (rule a)
   314 
   338 thm alpha.induct
       
   339 thm alpha_induct
   315 fun
   340 fun
   316   option_map::"('a \<Rightarrow> 'b) \<Rightarrow> ('a noption) \<Rightarrow> ('b noption)"
   341   option_map::"('a \<Rightarrow> 'b) \<Rightarrow> ('a noption) \<Rightarrow> ('b noption)"
   317 where
   342 where
   318   "option_map f (nSome x) = nSome (f x)"
   343   "option_map f (nSome x) = nSome (f x)"
   319 | "option_map f nNone = nNone"
   344 | "option_map f nNone = nNone"