3 

     4 function(sequential)

     5     akind :: "kind \<Rightarrow> kind \<Rightarrow> bool" ("_ \<approx>ki _" [100, 100] 100)

     6 and aty   :: "ty \<Rightarrow> ty \<Rightarrow> bool"     ("_ \<approx>ty _" [100, 100] 100)

     7 and atrm  :: "trm \<Rightarrow> trm \<Rightarrow> bool"   ("_ \<approx>tr _" [100, 100] 100)

     8 where

     9   a1: "(Type) \<approx>ki (Type) = True"

    10 | a2: "(KPi A x K) \<approx>ki (KPi A' x' K') = (A \<approx>ty A' \<and> (\<exists>pi. (rfv_kind K - {atom x} = rfv_kind K' - {atom x'} \<and> (rfv_kind K - {atom x})\<sharp>* pi \<and> (pi \<bullet> K) \<approx>ki K' \<and> (pi \<bullet> x) = x')))"

    11 | "_ \<approx>ki _ = False"

    12 | a3: "(TConst i) \<approx>ty (TConst j) = (i = j)"

    13 | a4: "(TApp A M) \<approx>ty (TApp A' M') = (A \<approx>ty A' \<and> M \<approx>tr M')"

    14 | a5: "(TPi A x B) \<approx>ty (TPi A' x' B') = ((A \<approx>ty A') \<and> (\<exists>pi. rfv_ty B - {atom x} = rfv_ty B' - {atom x'} \<and> (rfv_ty B - {atom x})\<sharp>* pi \<and> (pi \<bullet> B) \<approx>ty B' \<and> (pi \<bullet> x) = x'))"

    15 | "_ \<approx>ty _ = False"

    16 | a6: "(Const i) \<approx>tr (Const j) = (i = j)"

    17 | a7: "(Var x) \<approx>tr (Var y) = (x = y)"

    18 | a8: "(App M N) \<approx>tr (App M' N') = (M \<approx>tr M' \<and> N \<approx>tr N')"

    19 | a9: "(Lam A x M) \<approx>tr (Lam A' x' M') = (A \<approx>ty A' \<and> (\<exists>pi. rfv_trm M - {atom x} = rfv_trm M' - {atom x'} \<and> (rfv_trm M - {atom x})\<sharp>* pi \<and> (pi \<bullet> M) \<approx>tr M' \<and> (pi \<bullet> x) = x'))"

    20 | "_ \<approx>tr _ = False"

    21 apply (pat_completeness)

    22 apply simp_all

    23 done

    24 termination

    25 by (size_change)

    26 

    27 

    28 

    29 lemma regularize_to_injection:

    30   shows "(QUOT_TRUE l \<Longrightarrow> y) \<Longrightarrow> (l = r) \<longrightarrow> y"

    31   by(auto simp add: QUOT_TRUE_def)

    37 

    38 

    39 (* Atomize infrastructure *)

    40 (* FIXME/TODO: is this really needed? *)

    41 (*

    42 lemma atomize_eqv:

    43   shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)"

    44 proof

    45   assume "A \<equiv> B"

    46   then show "Trueprop A \<equiv> Trueprop B" by unfold

    47 next

    48   assume *: "Trueprop A \<equiv> Trueprop B"

    49   have "A = B"

    50   proof (cases A)

    51     case True

    52     have "A" by fact

    53     then show "A = B" using * by simp

    54   next

    55     case False

    56     have "\<not>A" by fact

    57     then show "A = B" using * by auto

    58   qed

    59   then show "A \<equiv> B" by (rule eq_reflection)

    60 qed

    61 *)

    62 

    63 

    64 ML {*

    65   fun dest_cbinop t =

    66     let

    67       val (t2, rhs) = Thm.dest_comb t;

    68       val (bop, lhs) = Thm.dest_comb t2;

    69     in

    70       (bop, (lhs, rhs))

    71     end

    72 *}

    73 

    74 ML {*

    75   fun dest_ceq t =

    76     let

    77       val (bop, pair) = dest_cbinop t;

    78       val (bop_s, _) = Term.dest_Const (Thm.term_of bop);

    79     in

    80       if bop_s = "op =" then pair else (raise CTERM ("Not an equality", [t]))

    81     end

    82 *}

    83 

    84 ML {*

    85   fun split_binop_conv t =

    86     let

    87       val (lhs, rhs) = dest_ceq t;

    88       val (bop, _) = dest_cbinop lhs;

    89       val [clT, cr2] = bop |> Thm.ctyp_of_term |> Thm.dest_ctyp;

    90       val [cmT, crT] = Thm.dest_ctyp cr2;

    91     in

    92       Drule.instantiate' [SOME clT, SOME cmT, SOME crT] [NONE, NONE, NONE, NONE, SOME bop] @{thm arg_cong2}

    93     end

    94 *}

    95 

    96 

    97 ML {*

    98   fun split_arg_conv t =

    99     let

   100       val (lhs, rhs) = dest_ceq t;

   101       val (lop, larg) = Thm.dest_comb lhs;

   102       val [caT, crT] = lop |> Thm.ctyp_of_term |> Thm.dest_ctyp;

   103     in

   104       Drule.instantiate' [SOME caT, SOME crT] [NONE, NONE, SOME lop] @{thm arg_cong}

   105     end

   106 *}

   107 

   108 ML {*

   109   fun split_binop_tac n thm =

   110     let

   111       val concl = Thm.cprem_of thm n;

   112       val (_, cconcl) = Thm.dest_comb concl;

   113       val rewr = split_binop_conv cconcl;

   114     in

   115       rtac rewr n thm

   116     end

   117       handle CTERM _ => Seq.empty

   118 *}

   119 

   120 

   121 ML {*

   122   fun split_arg_tac n thm =

   123     let

   124       val concl = Thm.cprem_of thm n;

   125       val (_, cconcl) = Thm.dest_comb concl;

   126       val rewr = split_arg_conv cconcl;

   127     in

   128       rtac rewr n thm

   129     end

   130       handle CTERM _ => Seq.empty

   131 *}

   132 

   133 

   134 lemma trueprop_cong:

   135   shows "(a \<equiv> b) \<Longrightarrow> (Trueprop a \<equiv> Trueprop b)"

   136   by auto

   137 

   138 lemma list_induct_hol4:

   139   fixes P :: "'a list \<Rightarrow> bool"

   140   assumes a: "((P []) \<and> (\<forall>t. (P t) \<longrightarrow> (\<forall>h. (P (h # t)))))"

   141   shows "\<forall>l. (P l)"

   142   using a

   143   apply (rule_tac allI)

   144   apply (induct_tac "l")

   145   apply (simp)

   146   apply (metis)

   147   done

   148 

   149 ML {*

   150 val no_vars = Thm.rule_attribute (fn context => fn th =>

   151   let

   152     val ctxt = Variable.set_body false (Context.proof_of context);

   153     val ((_, [th']), _) = Variable.import true [th] ctxt;

   154   in th' end);

   155 *}

   156 

   157 (*lemma equality_twice:

   158   "a = c \<Longrightarrow> b = d \<Longrightarrow> (a = b \<longrightarrow> c = d)"

   159 by auto*)

   160