Nominal/Rsp.thy
author Cezary Kaliszyk <kaliszyk@in.tum.de>
Sat, 27 Mar 2010 13:50:59 +0100
changeset 1681 b8a07a3c1692
parent 1673 e8cf0520c820
child 1683 f78c820f67c3
permissions -rw-r--r--
Get lifted types information from the quotient package.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1227
ec2e0116779e rsp infrastructure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     1
theory Rsp
1653
a2142526bb01 Removed another cheat and cleaned the code a bit.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1650
diff changeset
     2
imports Abs Tacs
1227
ec2e0116779e rsp infrastructure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     3
begin
ec2e0116779e rsp infrastructure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     4
ec2e0116779e rsp infrastructure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     5
ML {*
1230
a41c3a105104 rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1227
diff changeset
     6
fun const_rsp lthy const =
1227
ec2e0116779e rsp infrastructure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     7
let
ec2e0116779e rsp infrastructure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     8
  val nty = fastype_of (Quotient_Term.quotient_lift_const ("", const) lthy)
ec2e0116779e rsp infrastructure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     9
  val rel = Quotient_Term.equiv_relation_chk lthy (fastype_of const, nty);
ec2e0116779e rsp infrastructure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    10
in
ec2e0116779e rsp infrastructure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    11
  HOLogic.mk_Trueprop (rel $ const $ const)
ec2e0116779e rsp infrastructure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    12
end
ec2e0116779e rsp infrastructure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    13
*}
ec2e0116779e rsp infrastructure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    14
1230
a41c3a105104 rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1227
diff changeset
    15
(* Replaces bounds by frees and meta implications by implications *)
1227
ec2e0116779e rsp infrastructure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    16
ML {*
1230
a41c3a105104 rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1227
diff changeset
    17
fun prepare_goal trm =
1227
ec2e0116779e rsp infrastructure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    18
let
ec2e0116779e rsp infrastructure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    19
  val vars = strip_all_vars trm
ec2e0116779e rsp infrastructure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    20
  val fs = rev (map Free vars)
1230
a41c3a105104 rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1227
diff changeset
    21
  val (fixes, no_alls) = ((map fst vars), subst_bounds (fs, (strip_all_body trm)))
a41c3a105104 rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1227
diff changeset
    22
  val prems = map HOLogic.dest_Trueprop (Logic.strip_imp_prems no_alls)
a41c3a105104 rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1227
diff changeset
    23
  val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl no_alls)
1227
ec2e0116779e rsp infrastructure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    24
in
1230
a41c3a105104 rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1227
diff changeset
    25
  (fixes, fold (curry HOLogic.mk_imp) prems concl)
1227
ec2e0116779e rsp infrastructure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    26
end
ec2e0116779e rsp infrastructure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    27
*}
ec2e0116779e rsp infrastructure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    28
ec2e0116779e rsp infrastructure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    29
ML {*
ec2e0116779e rsp infrastructure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    30
fun get_rsp_goal thy trm =
ec2e0116779e rsp infrastructure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    31
let
ec2e0116779e rsp infrastructure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    32
  val goalstate = Goal.init (cterm_of thy trm);
ec2e0116779e rsp infrastructure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    33
  val tac = REPEAT o rtac @{thm fun_rel_id};
ec2e0116779e rsp infrastructure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    34
in
ec2e0116779e rsp infrastructure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    35
  case (SINGLE (tac 1) goalstate) of
ec2e0116779e rsp infrastructure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    36
    NONE => error "rsp_goal failed"
1230
a41c3a105104 rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1227
diff changeset
    37
  | SOME th => prepare_goal (term_of (cprem_of th 1))
1227
ec2e0116779e rsp infrastructure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    38
end
ec2e0116779e rsp infrastructure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    39
*}
ec2e0116779e rsp infrastructure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    40
ec2e0116779e rsp infrastructure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    41
ML {*
1230
a41c3a105104 rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1227
diff changeset
    42
fun prove_const_rsp bind consts tac ctxt =
1227
ec2e0116779e rsp infrastructure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    43
let
1230
a41c3a105104 rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1227
diff changeset
    44
  val rsp_goals = map (const_rsp ctxt) consts
1227
ec2e0116779e rsp infrastructure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    45
  val thy = ProofContext.theory_of ctxt
1230
a41c3a105104 rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1227
diff changeset
    46
  val (fixed, user_goals) = split_list (map (get_rsp_goal thy) rsp_goals)
a41c3a105104 rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1227
diff changeset
    47
  val fixed' = distinct (op =) (flat fixed)
a41c3a105104 rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1227
diff changeset
    48
  val user_goal = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj user_goals)
a41c3a105104 rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1227
diff changeset
    49
  val user_thm = Goal.prove ctxt fixed' [] user_goal tac
a41c3a105104 rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1227
diff changeset
    50
  val user_thms = map repeat_mp (HOLogic.conj_elims user_thm)
a41c3a105104 rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1227
diff changeset
    51
  fun tac _ = (REPEAT o rtac @{thm fun_rel_id} THEN' resolve_tac user_thms THEN_ALL_NEW atac) 1
a41c3a105104 rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1227
diff changeset
    52
  val rsp_thms = map (fn gl => Goal.prove ctxt [] [] gl tac) rsp_goals
1227
ec2e0116779e rsp infrastructure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    53
in
ec2e0116779e rsp infrastructure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    54
   ctxt
ec2e0116779e rsp infrastructure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    55
|> snd o Local_Theory.note 
1230
a41c3a105104 rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1227
diff changeset
    56
  ((Binding.empty, [Attrib.internal (fn _ => Quotient_Info.rsp_rules_add)]), rsp_thms)
1278
8814494fe4da Change in signature of prove_const_rsp for general lifting.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1268
diff changeset
    57
|> Local_Theory.note ((bind, []), user_thms)
1227
ec2e0116779e rsp infrastructure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    58
end
ec2e0116779e rsp infrastructure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    59
*}
ec2e0116779e rsp infrastructure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    60
1573
b39108f42638 fv_rsp proved automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
    61
ML {*
b39108f42638 fv_rsp proved automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
    62
fun fvbv_rsp_tac induct fvbv_simps ctxt =
1653
a2142526bb01 Removed another cheat and cleaned the code a bit.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1650
diff changeset
    63
  rel_indtac induct THEN_ALL_NEW
1573
b39108f42638 fv_rsp proved automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
    64
  (TRY o rtac @{thm TrueI}) THEN_ALL_NEW
1673
e8cf0520c820 New compose lemmas. Reverted alpha_gen sym/trans changes. Equivp for alpha_res should work now.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1672
diff changeset
    65
  asm_full_simp_tac (HOL_basic_ss addsimps @{thms alphas2}) THEN_ALL_NEW
1672
94b8b70f7bc0 Initial proof modifications for alpha_res
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1656
diff changeset
    66
  asm_full_simp_tac (HOL_ss addsimps (@{thms alphas} @ fvbv_simps)) THEN_ALL_NEW
1573
b39108f42638 fv_rsp proved automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
    67
  REPEAT o eresolve_tac [conjE, exE] THEN_ALL_NEW
b39108f42638 fv_rsp proved automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
    68
  asm_full_simp_tac (HOL_ss addsimps fvbv_simps) THEN_ALL_NEW
b39108f42638 fv_rsp proved automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
    69
  TRY o blast_tac (claset_of ctxt)
1227
ec2e0116779e rsp infrastructure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    70
*}
ec2e0116779e rsp infrastructure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    71
ec2e0116779e rsp infrastructure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    72
ML {*
1553
4355eb3b7161 Automatically derive support for datatypes with at-most one binding per constructor.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1494
diff changeset
    73
fun sym_eqvts ctxt = map (fn x => sym OF [x]) (Nominal_ThmDecls.get_eqvts_thms ctxt)
4355eb3b7161 Automatically derive support for datatypes with at-most one binding per constructor.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1494
diff changeset
    74
fun all_eqvts ctxt =
4355eb3b7161 Automatically derive support for datatypes with at-most one binding per constructor.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1494
diff changeset
    75
  Nominal_ThmDecls.get_eqvts_thms ctxt @ Nominal_ThmDecls.get_eqvts_raw_thms ctxt
1416
947e5f772a9c Lifting constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1410
diff changeset
    76
*}
947e5f772a9c Lifting constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1410
diff changeset
    77
947e5f772a9c Lifting constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1410
diff changeset
    78
ML {*
1561
c3dca6e600c8 Use 'alpha_bn_refl' to get rid of one of the sorrys.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1553
diff changeset
    79
fun constr_rsp_tac inj rsp =
1230
a41c3a105104 rsp for bv; the only issue is that it requires an appropriate induction principle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1227
diff changeset
    80
  REPEAT o rtac impI THEN'
1653
a2142526bb01 Removed another cheat and cleaned the code a bit.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1650
diff changeset
    81
  simp_tac (HOL_ss addsimps inj) THEN' split_conj_tac THEN_ALL_NEW
1227
ec2e0116779e rsp infrastructure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    82
  (asm_simp_tac HOL_ss THEN_ALL_NEW (
1561
c3dca6e600c8 Use 'alpha_bn_refl' to get rid of one of the sorrys.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1553
diff changeset
    83
   REPEAT o rtac @{thm exI[of _ "0 :: perm"]} THEN_ALL_NEW
1673
e8cf0520c820 New compose lemmas. Reverted alpha_gen sym/trans changes. Equivp for alpha_res should work now.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1672
diff changeset
    84
   simp_tac (HOL_basic_ss addsimps @{thms alphas2}) THEN_ALL_NEW
1561
c3dca6e600c8 Use 'alpha_bn_refl' to get rid of one of the sorrys.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1553
diff changeset
    85
   asm_full_simp_tac (HOL_ss addsimps (rsp @
1672
94b8b70f7bc0 Initial proof modifications for alpha_res
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1656
diff changeset
    86
     @{thms alphas fresh_star_def fresh_zero_perm permute_zero ball_triv add_0_left}))
1227
ec2e0116779e rsp infrastructure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    87
  ))
ec2e0116779e rsp infrastructure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    88
*}
ec2e0116779e rsp infrastructure.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    89
1268
d1999540d23a Move the eqvt code out of Terms and fixed induction for single-rule examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1258
diff changeset
    90
ML {*
1445
3246c5e1a9d7 cheat_alpha_eqvt no longer needed; the proofs work.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1416
diff changeset
    91
fun perm_arg arg =
3246c5e1a9d7 cheat_alpha_eqvt no longer needed; the proofs work.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1416
diff changeset
    92
let
3246c5e1a9d7 cheat_alpha_eqvt no longer needed; the proofs work.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1416
diff changeset
    93
  val ty = fastype_of arg
3246c5e1a9d7 cheat_alpha_eqvt no longer needed; the proofs work.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1416
diff changeset
    94
in
3246c5e1a9d7 cheat_alpha_eqvt no longer needed; the proofs work.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1416
diff changeset
    95
  Const (@{const_name permute}, @{typ perm} --> ty --> ty)
3246c5e1a9d7 cheat_alpha_eqvt no longer needed; the proofs work.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1416
diff changeset
    96
end
1268
d1999540d23a Move the eqvt code out of Terms and fixed induction for single-rule examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1258
diff changeset
    97
*}
d1999540d23a Move the eqvt code out of Terms and fixed induction for single-rule examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1258
diff changeset
    98
1300
22a084c9316b Fixed eqvt code.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1278
diff changeset
    99
lemma exi: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (pi \<bullet> p)) \<Longrightarrow> \<exists>pi. Q pi"
22a084c9316b Fixed eqvt code.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1278
diff changeset
   100
apply (erule exE)
22a084c9316b Fixed eqvt code.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1278
diff changeset
   101
apply (rule_tac x="pi \<bullet> pia" in exI)
22a084c9316b Fixed eqvt code.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1278
diff changeset
   102
by auto
1268
d1999540d23a Move the eqvt code out of Terms and fixed induction for single-rule examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1258
diff changeset
   103
1331
0f329449e304 Fix eqvt for multiple quantifiers.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1314
diff changeset
   104
0f329449e304 Fix eqvt for multiple quantifiers.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1314
diff changeset
   105
ML {*
0f329449e304 Fix eqvt for multiple quantifiers.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1314
diff changeset
   106
fun alpha_eqvt_tac induct simps ctxt =
1653
a2142526bb01 Removed another cheat and cleaned the code a bit.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1650
diff changeset
   107
  rel_indtac induct THEN_ALL_NEW
1656
c9d3dda79fe3 Removed remaining cheats + some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1653
diff changeset
   108
  simp_tac (HOL_basic_ss addsimps simps) THEN_ALL_NEW
1653
a2142526bb01 Removed another cheat and cleaned the code a bit.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1650
diff changeset
   109
  REPEAT o etac @{thm exi[of _ _ "p"]} THEN' split_conj_tac THEN_ALL_NEW
1331
0f329449e304 Fix eqvt for multiple quantifiers.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1314
diff changeset
   110
  asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ simps)) THEN_ALL_NEW
0f329449e304 Fix eqvt for multiple quantifiers.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1314
diff changeset
   111
  asm_full_simp_tac (HOL_ss addsimps 
1672
94b8b70f7bc0 Initial proof modifications for alpha_res
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1656
diff changeset
   112
    @{thms supp_eqvt[symmetric] inter_eqvt[symmetric] empty_eqvt alphas}) THEN_ALL_NEW
1653
a2142526bb01 Removed another cheat and cleaned the code a bit.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1650
diff changeset
   113
  (split_conj_tac THEN_ALL_NEW TRY o resolve_tac
1331
0f329449e304 Fix eqvt for multiple quantifiers.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1314
diff changeset
   114
    @{thms fresh_star_permute_iff[of "- p", THEN iffD1] permute_eq_iff[of "- p", THEN iffD1]})
0f329449e304 Fix eqvt for multiple quantifiers.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1314
diff changeset
   115
  THEN_ALL_NEW
1494
923413256cbb Clean 'Lift', start working only on exported things in Parser.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1474
diff changeset
   116
  asm_full_simp_tac (HOL_ss addsimps (@{thms split_conv permute_minus_cancel permute_plus permute_eqvt[symmetric]} @ all_eqvts ctxt @ simps))
1331
0f329449e304 Fix eqvt for multiple quantifiers.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1314
diff changeset
   117
*}
0f329449e304 Fix eqvt for multiple quantifiers.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1314
diff changeset
   118
0f329449e304 Fix eqvt for multiple quantifiers.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1314
diff changeset
   119
ML {*
1445
3246c5e1a9d7 cheat_alpha_eqvt no longer needed; the proofs work.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1416
diff changeset
   120
fun build_alpha_eqvt alpha names =
1268
d1999540d23a Move the eqvt code out of Terms and fixed induction for single-rule examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1258
diff changeset
   121
let
d1999540d23a Move the eqvt code out of Terms and fixed induction for single-rule examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1258
diff changeset
   122
  val pi = Free ("p", @{typ perm});
1445
3246c5e1a9d7 cheat_alpha_eqvt no longer needed; the proofs work.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1416
diff changeset
   123
  val (tys, _) = strip_type (fastype_of alpha)
3246c5e1a9d7 cheat_alpha_eqvt no longer needed; the proofs work.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1416
diff changeset
   124
  val indnames = Name.variant_list names (Datatype_Prop.make_tnames (map body_type tys));
3246c5e1a9d7 cheat_alpha_eqvt no longer needed; the proofs work.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1416
diff changeset
   125
  val args = map Free (indnames ~~ tys);
3246c5e1a9d7 cheat_alpha_eqvt no longer needed; the proofs work.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1416
diff changeset
   126
  val perm_args = map (fn x => perm_arg x $ pi $ x) args
3246c5e1a9d7 cheat_alpha_eqvt no longer needed; the proofs work.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1416
diff changeset
   127
in
3246c5e1a9d7 cheat_alpha_eqvt no longer needed; the proofs work.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1416
diff changeset
   128
  (HOLogic.mk_imp (list_comb (alpha, args), list_comb (alpha, perm_args)), indnames @ names)
3246c5e1a9d7 cheat_alpha_eqvt no longer needed; the proofs work.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1416
diff changeset
   129
end
3246c5e1a9d7 cheat_alpha_eqvt no longer needed; the proofs work.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1416
diff changeset
   130
*}
3246c5e1a9d7 cheat_alpha_eqvt no longer needed; the proofs work.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1416
diff changeset
   131
3246c5e1a9d7 cheat_alpha_eqvt no longer needed; the proofs work.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1416
diff changeset
   132
ML {*
3246c5e1a9d7 cheat_alpha_eqvt no longer needed; the proofs work.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1416
diff changeset
   133
fun build_alpha_eqvts funs tac ctxt =
3246c5e1a9d7 cheat_alpha_eqvt no longer needed; the proofs work.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1416
diff changeset
   134
let
3246c5e1a9d7 cheat_alpha_eqvt no longer needed; the proofs work.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1416
diff changeset
   135
  val (gls, names) = fold_map build_alpha_eqvt funs ["p"]
3246c5e1a9d7 cheat_alpha_eqvt no longer needed; the proofs work.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1416
diff changeset
   136
  val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj gls)
3246c5e1a9d7 cheat_alpha_eqvt no longer needed; the proofs work.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1416
diff changeset
   137
  val thm = Goal.prove ctxt names [] gl tac
1268
d1999540d23a Move the eqvt code out of Terms and fixed induction for single-rule examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1258
diff changeset
   138
in
d1999540d23a Move the eqvt code out of Terms and fixed induction for single-rule examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1258
diff changeset
   139
  map (fn x => mp OF [x]) (HOLogic.conj_elims thm)
d1999540d23a Move the eqvt code out of Terms and fixed induction for single-rule examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1258
diff changeset
   140
end
d1999540d23a Move the eqvt code out of Terms and fixed induction for single-rule examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1258
diff changeset
   141
*}
d1999540d23a Move the eqvt code out of Terms and fixed induction for single-rule examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1258
diff changeset
   142
1308
80dabcaafc38 Moving wrappers out of Lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1303
diff changeset
   143
ML {*
1573
b39108f42638 fv_rsp proved automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
   144
fun prove_fv_rsp fv_alphas_lst all_alphas tac ctxt =
b39108f42638 fv_rsp proved automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
   145
let
b39108f42638 fv_rsp proved automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
   146
  val (fvs_alphas, ls) = split_list fv_alphas_lst;
b39108f42638 fv_rsp proved automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
   147
  val (fv_ts, alpha_ts) = split_list fvs_alphas;
b39108f42638 fv_rsp proved automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
   148
  val tys = map (domain_type o fastype_of) alpha_ts;
b39108f42638 fv_rsp proved automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
   149
  val names = Datatype_Prop.make_tnames tys;
b39108f42638 fv_rsp proved automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
   150
  val names2 = Name.variant_list names names;
b39108f42638 fv_rsp proved automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
   151
  val args = map Free (names ~~ tys);
b39108f42638 fv_rsp proved automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
   152
  val args2 = map Free (names2 ~~ tys);
b39108f42638 fv_rsp proved automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
   153
  fun mk_fv_rsp arg arg2 (fv, alpha) = HOLogic.mk_eq ((fv $ arg), (fv $ arg2));
b39108f42638 fv_rsp proved automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
   154
  fun fv_rsp_arg (((fv, alpha), (arg, arg2)), l) =
b39108f42638 fv_rsp proved automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
   155
    HOLogic.mk_imp (
b39108f42638 fv_rsp proved automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
   156
     (alpha $ arg $ arg2),
b39108f42638 fv_rsp proved automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
   157
     (foldr1 HOLogic.mk_conj
b39108f42638 fv_rsp proved automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
   158
       (HOLogic.mk_eq (fv $ arg, fv $ arg2) ::
b39108f42638 fv_rsp proved automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
   159
       (map (mk_fv_rsp arg arg2) l))));
b39108f42638 fv_rsp proved automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
   160
  val nobn_eqs = map fv_rsp_arg (((fv_ts ~~ alpha_ts) ~~ (args ~~ args2)) ~~ ls);
b39108f42638 fv_rsp proved automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
   161
  fun mk_fv_rsp_bn arg arg2 (fv, alpha) =
b39108f42638 fv_rsp proved automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
   162
    HOLogic.mk_imp (
b39108f42638 fv_rsp proved automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
   163
      (alpha $ arg $ arg2),
b39108f42638 fv_rsp proved automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
   164
      HOLogic.mk_eq ((fv $ arg), (fv $ arg2)));
b39108f42638 fv_rsp proved automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
   165
  fun fv_rsp_arg_bn ((arg, arg2), l) =
b39108f42638 fv_rsp proved automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
   166
    map (mk_fv_rsp_bn arg arg2) l;
b39108f42638 fv_rsp proved automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
   167
  val bn_eqs = flat (map fv_rsp_arg_bn ((args ~~ args2) ~~ ls));
b39108f42638 fv_rsp proved automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
   168
  val (_, add_alphas) = chop (length (nobn_eqs @ bn_eqs)) all_alphas;
b39108f42638 fv_rsp proved automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
   169
  val atys = map (domain_type o fastype_of) add_alphas;
b39108f42638 fv_rsp proved automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
   170
  val anames = Name.variant_list (names @ names2) (Datatype_Prop.make_tnames atys);
b39108f42638 fv_rsp proved automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
   171
  val aargs = map Free (anames ~~ atys);
b39108f42638 fv_rsp proved automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
   172
  val aeqs = map2 (fn alpha => fn arg => HOLogic.mk_imp (alpha $ arg $ arg, @{term True}))
b39108f42638 fv_rsp proved automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
   173
    add_alphas aargs;
b39108f42638 fv_rsp proved automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
   174
  val eq = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (nobn_eqs @ bn_eqs @ aeqs));
b39108f42638 fv_rsp proved automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
   175
  val th = Goal.prove ctxt (names @ names2) [] eq tac;
b39108f42638 fv_rsp proved automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
   176
  val ths = HOLogic.conj_elims th;
b39108f42638 fv_rsp proved automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
   177
  val (ths_nobn, ths_bn) = chop (length ls) ths;
b39108f42638 fv_rsp proved automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
   178
  fun project (th, l) =
b39108f42638 fv_rsp proved automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
   179
    Project_Rule.projects ctxt (1 upto (length l + 1)) (hd (Project_Rule.projections ctxt th))
b39108f42638 fv_rsp proved automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
   180
  val ths_nobn_pr = map project (ths_nobn ~~ ls);
b39108f42638 fv_rsp proved automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
   181
in
b39108f42638 fv_rsp proved automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
   182
  (flat ths_nobn_pr @ ths_bn)
1268
d1999540d23a Move the eqvt code out of Terms and fixed induction for single-rule examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1258
diff changeset
   183
end
1573
b39108f42638 fv_rsp proved automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
   184
*}
b39108f42638 fv_rsp proved automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
   185
1653
a2142526bb01 Removed another cheat and cleaned the code a bit.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1650
diff changeset
   186
(** alpha_bn_rsp **)
a2142526bb01 Removed another cheat and cleaned the code a bit.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1650
diff changeset
   187
1575
2c37f5a8c747 alpha_bn_rsp_pre automatized.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1573
diff changeset
   188
lemma equivp_rspl:
2c37f5a8c747 alpha_bn_rsp_pre automatized.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1573
diff changeset
   189
  "equivp r \<Longrightarrow> r a b \<Longrightarrow> r a c = r b c"
2c37f5a8c747 alpha_bn_rsp_pre automatized.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1573
diff changeset
   190
  unfolding equivp_reflp_symp_transp symp_def transp_def 
2c37f5a8c747 alpha_bn_rsp_pre automatized.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1573
diff changeset
   191
  by blast
2c37f5a8c747 alpha_bn_rsp_pre automatized.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1573
diff changeset
   192
2c37f5a8c747 alpha_bn_rsp_pre automatized.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1573
diff changeset
   193
lemma equivp_rspr:
2c37f5a8c747 alpha_bn_rsp_pre automatized.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1573
diff changeset
   194
  "equivp r \<Longrightarrow> r a b \<Longrightarrow> r c a = r c b"
2c37f5a8c747 alpha_bn_rsp_pre automatized.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1573
diff changeset
   195
  unfolding equivp_reflp_symp_transp symp_def transp_def 
2c37f5a8c747 alpha_bn_rsp_pre automatized.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1573
diff changeset
   196
  by blast
2c37f5a8c747 alpha_bn_rsp_pre automatized.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1573
diff changeset
   197
2c37f5a8c747 alpha_bn_rsp_pre automatized.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1573
diff changeset
   198
ML {*
1653
a2142526bb01 Removed another cheat and cleaned the code a bit.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1650
diff changeset
   199
fun alpha_bn_rsp_tac simps res exhausts a ctxt =
a2142526bb01 Removed another cheat and cleaned the code a bit.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1650
diff changeset
   200
  rtac allI THEN_ALL_NEW
a2142526bb01 Removed another cheat and cleaned the code a bit.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1650
diff changeset
   201
  case_rules_tac ctxt a exhausts THEN_ALL_NEW
a2142526bb01 Removed another cheat and cleaned the code a bit.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1650
diff changeset
   202
  asm_full_simp_tac (HOL_ss addsimps simps) THEN_ALL_NEW
a2142526bb01 Removed another cheat and cleaned the code a bit.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1650
diff changeset
   203
  TRY o REPEAT_ALL_NEW (rtac @{thm arg_cong2[of _ _ _ _ "op \<and>"]}) THEN_ALL_NEW
a2142526bb01 Removed another cheat and cleaned the code a bit.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1650
diff changeset
   204
  TRY o eresolve_tac res THEN_ALL_NEW
a2142526bb01 Removed another cheat and cleaned the code a bit.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1650
diff changeset
   205
  asm_full_simp_tac (HOL_ss addsimps simps);
a2142526bb01 Removed another cheat and cleaned the code a bit.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1650
diff changeset
   206
*}
a2142526bb01 Removed another cheat and cleaned the code a bit.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1650
diff changeset
   207
a2142526bb01 Removed another cheat and cleaned the code a bit.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1650
diff changeset
   208
a2142526bb01 Removed another cheat and cleaned the code a bit.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1650
diff changeset
   209
ML {*
a2142526bb01 Removed another cheat and cleaned the code a bit.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1650
diff changeset
   210
fun build_alpha_bn_rsp_gl a alphas alpha_bn ctxt =
1575
2c37f5a8c747 alpha_bn_rsp_pre automatized.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1573
diff changeset
   211
let
1653
a2142526bb01 Removed another cheat and cleaned the code a bit.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1650
diff changeset
   212
  val ty = domain_type (fastype_of alpha_bn);
a2142526bb01 Removed another cheat and cleaned the code a bit.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1650
diff changeset
   213
  val (l, r) = the (AList.lookup (op=) alphas ty);
1575
2c37f5a8c747 alpha_bn_rsp_pre automatized.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1573
diff changeset
   214
in
1653
a2142526bb01 Removed another cheat and cleaned the code a bit.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1650
diff changeset
   215
  ([HOLogic.mk_all (a, ty, HOLogic.mk_eq (alpha_bn $ l $ Bound 0, alpha_bn $ r $ Bound 0)),
a2142526bb01 Removed another cheat and cleaned the code a bit.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1650
diff changeset
   216
    HOLogic.mk_all (a, ty, HOLogic.mk_eq (alpha_bn $ Bound 0 $ l, alpha_bn $ Bound 0 $ r))], ctxt)
1575
2c37f5a8c747 alpha_bn_rsp_pre automatized.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1573
diff changeset
   217
end
2c37f5a8c747 alpha_bn_rsp_pre automatized.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1573
diff changeset
   218
*}
2c37f5a8c747 alpha_bn_rsp_pre automatized.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1573
diff changeset
   219
1653
a2142526bb01 Removed another cheat and cleaned the code a bit.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1650
diff changeset
   220
ML {*
a2142526bb01 Removed another cheat and cleaned the code a bit.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1650
diff changeset
   221
fun prove_alpha_bn_rsp alphas ind simps equivps exhausts alpha_bns ctxt =
a2142526bb01 Removed another cheat and cleaned the code a bit.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1650
diff changeset
   222
let
a2142526bb01 Removed another cheat and cleaned the code a bit.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1650
diff changeset
   223
  val ([a], ctxt') = Variable.variant_fixes ["a"] ctxt;
a2142526bb01 Removed another cheat and cleaned the code a bit.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1650
diff changeset
   224
  val resl = map (fn x => @{thm equivp_rspl} OF [x]) equivps;
a2142526bb01 Removed another cheat and cleaned the code a bit.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1650
diff changeset
   225
  val resr = map (fn x => @{thm equivp_rspr} OF [x]) equivps;
a2142526bb01 Removed another cheat and cleaned the code a bit.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1650
diff changeset
   226
  val ths_loc = prove_by_rel_induct alphas (build_alpha_bn_rsp_gl a) ind
a2142526bb01 Removed another cheat and cleaned the code a bit.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1650
diff changeset
   227
    (alpha_bn_rsp_tac simps (resl @ resr) exhausts a) alpha_bns ctxt
a2142526bb01 Removed another cheat and cleaned the code a bit.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1650
diff changeset
   228
in
a2142526bb01 Removed another cheat and cleaned the code a bit.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1650
diff changeset
   229
  Variable.export ctxt' ctxt ths_loc
a2142526bb01 Removed another cheat and cleaned the code a bit.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1650
diff changeset
   230
end
a2142526bb01 Removed another cheat and cleaned the code a bit.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1650
diff changeset
   231
*}
1573
b39108f42638 fv_rsp proved automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
   232
1656
c9d3dda79fe3 Removed remaining cheats + some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1653
diff changeset
   233
ML {*
c9d3dda79fe3 Removed remaining cheats + some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1653
diff changeset
   234
fun build_alpha_alpha_bn_gl alphas alpha_bn ctxt =
c9d3dda79fe3 Removed remaining cheats + some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1653
diff changeset
   235
let
c9d3dda79fe3 Removed remaining cheats + some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1653
diff changeset
   236
  val ty = domain_type (fastype_of alpha_bn);
c9d3dda79fe3 Removed remaining cheats + some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1653
diff changeset
   237
  val (l, r) = the (AList.lookup (op=) alphas ty);
c9d3dda79fe3 Removed remaining cheats + some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1653
diff changeset
   238
in
c9d3dda79fe3 Removed remaining cheats + some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1653
diff changeset
   239
  ([alpha_bn $ l $ r], ctxt)
1573
b39108f42638 fv_rsp proved automatically.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1561
diff changeset
   240
end
1656
c9d3dda79fe3 Removed remaining cheats + some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1653
diff changeset
   241
*}
c9d3dda79fe3 Removed remaining cheats + some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1653
diff changeset
   242
c9d3dda79fe3 Removed remaining cheats + some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1653
diff changeset
   243
ML {*
c9d3dda79fe3 Removed remaining cheats + some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1653
diff changeset
   244
fun prove_alpha_alphabn alphas ind simps alpha_bns ctxt =
c9d3dda79fe3 Removed remaining cheats + some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1653
diff changeset
   245
  prove_by_rel_induct alphas build_alpha_alpha_bn_gl ind
c9d3dda79fe3 Removed remaining cheats + some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1653
diff changeset
   246
    (fn _ => asm_full_simp_tac (HOL_ss addsimps simps)) alpha_bns ctxt
c9d3dda79fe3 Removed remaining cheats + some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1653
diff changeset
   247
*}
c9d3dda79fe3 Removed remaining cheats + some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1653
diff changeset
   248
c9d3dda79fe3 Removed remaining cheats + some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1653
diff changeset
   249
ML {*
c9d3dda79fe3 Removed remaining cheats + some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1653
diff changeset
   250
fun build_rsp_gl alphas fnctn ctxt =
c9d3dda79fe3 Removed remaining cheats + some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1653
diff changeset
   251
let
c9d3dda79fe3 Removed remaining cheats + some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1653
diff changeset
   252
  val typ = domain_type (fastype_of fnctn);
c9d3dda79fe3 Removed remaining cheats + some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1653
diff changeset
   253
  val (argl, argr) = the (AList.lookup (op=) alphas typ);
c9d3dda79fe3 Removed remaining cheats + some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1653
diff changeset
   254
in
c9d3dda79fe3 Removed remaining cheats + some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1653
diff changeset
   255
  ([HOLogic.mk_eq (fnctn $ argl, fnctn $ argr)], ctxt)
c9d3dda79fe3 Removed remaining cheats + some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1653
diff changeset
   256
end
c9d3dda79fe3 Removed remaining cheats + some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1653
diff changeset
   257
*}
c9d3dda79fe3 Removed remaining cheats + some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1653
diff changeset
   258
c9d3dda79fe3 Removed remaining cheats + some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1653
diff changeset
   259
ML {*
c9d3dda79fe3 Removed remaining cheats + some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1653
diff changeset
   260
fun fvbv_rsp_tac' simps ctxt =
1673
e8cf0520c820 New compose lemmas. Reverted alpha_gen sym/trans changes. Equivp for alpha_res should work now.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1672
diff changeset
   261
  asm_full_simp_tac (HOL_basic_ss addsimps @{thms alphas2}) THEN_ALL_NEW
1672
94b8b70f7bc0 Initial proof modifications for alpha_res
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1656
diff changeset
   262
  asm_full_simp_tac (HOL_ss addsimps (@{thms alphas} @ simps)) THEN_ALL_NEW
1656
c9d3dda79fe3 Removed remaining cheats + some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1653
diff changeset
   263
  REPEAT o eresolve_tac [conjE, exE] THEN_ALL_NEW
c9d3dda79fe3 Removed remaining cheats + some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1653
diff changeset
   264
  asm_full_simp_tac (HOL_ss addsimps simps) THEN_ALL_NEW
c9d3dda79fe3 Removed remaining cheats + some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1653
diff changeset
   265
  TRY o blast_tac (claset_of ctxt)
c9d3dda79fe3 Removed remaining cheats + some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1653
diff changeset
   266
*}
c9d3dda79fe3 Removed remaining cheats + some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1653
diff changeset
   267
c9d3dda79fe3 Removed remaining cheats + some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1653
diff changeset
   268
ML {*
c9d3dda79fe3 Removed remaining cheats + some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1653
diff changeset
   269
fun build_fvbv_rsps alphas ind simps fnctns ctxt =
c9d3dda79fe3 Removed remaining cheats + some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1653
diff changeset
   270
  prove_by_rel_induct alphas build_rsp_gl ind (fvbv_rsp_tac' simps) fnctns ctxt
c9d3dda79fe3 Removed remaining cheats + some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1653
diff changeset
   271
*}
c9d3dda79fe3 Removed remaining cheats + some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1653
diff changeset
   272
c9d3dda79fe3 Removed remaining cheats + some cleaning.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1653
diff changeset
   273
end