equal
deleted
inserted
replaced
1003 in |
1003 in |
1004 lthy' |> note_many mut_name ((@{binding "intros"}, []), intro_rules) |
1004 lthy' |> note_many mut_name ((@{binding "intros"}, []), intro_rules) |
1005 ||>> note_many mut_name ((@{binding "inducts"}, []), ind_prins) |
1005 ||>> note_many mut_name ((@{binding "inducts"}, []), ind_prins) |
1006 ||>> fold_map (note_single1 mut_name) (namesattrs ~~ intro_rules) |
1006 ||>> fold_map (note_single1 mut_name) (namesattrs ~~ intro_rules) |
1007 ||>> fold_map (note_single2 @{binding "induct"} |
1007 ||>> fold_map (note_single2 @{binding "induct"} |
1008 [Attrib.internal (K (RuleCases.case_names case_names)), |
1008 [Attrib.internal (K (Rule_Cases.case_names case_names)), |
1009 Attrib.internal (K (RuleCases.consumes 1)), |
1009 Attrib.internal (K (Rule_Cases.consumes 1)), |
1010 Attrib.internal (K (Induct.induct_pred ""))]) |
1010 Attrib.internal (K (Induct.induct_pred ""))]) |
1011 (prednames ~~ ind_prins) |
1011 (prednames ~~ ind_prins) |
1012 |> snd |
1012 |> snd |
1013 end*} |
1013 end*} |
1014 |
1014 |
1041 @{text "mut_name.inducts"}, respectively (see previous paragraph). |
1041 @{text "mut_name.inducts"}, respectively (see previous paragraph). |
1042 |
1042 |
1043 Line 20 add further every introduction rule under its own name |
1043 Line 20 add further every introduction rule under its own name |
1044 (given by the user).\footnote{FIXME: what happens if the user did not give |
1044 (given by the user).\footnote{FIXME: what happens if the user did not give |
1045 any name.} Line 21 registers the induction principles. For this we have |
1045 any name.} Line 21 registers the induction principles. For this we have |
1046 to use some specific attributes. The first @{ML_ind case_names in RuleCases} |
1046 to use some specific attributes. The first @{ML_ind case_names in Rule_Cases} |
1047 corresponds to the case names that are used by Isar to reference the proof |
1047 corresponds to the case names that are used by Isar to reference the proof |
1048 obligations in the induction. The second @{ML "consumes 1" in RuleCases} |
1048 obligations in the induction. The second @{ML "consumes 1" in Rule_Cases} |
1049 indicates that the first premise of the induction principle (namely |
1049 indicates that the first premise of the induction principle (namely |
1050 the predicate over which the induction proceeds) is eliminated. |
1050 the predicate over which the induction proceeds) is eliminated. |
1051 |
1051 |
1052 This completes all the code and fits in with the ``front end'' described |
1052 This completes all the code and fits in with the ``front end'' described |
1053 in Section~\ref{sec:interface}.\footnote{FIXME: Describe @{ML Induct.induct_pred}. |
1053 in Section~\ref{sec:interface}.\footnote{FIXME: Describe @{ML Induct.induct_pred}. |